Types themselves are not proofs. In particular, the proposition associated to a type might be a blatant lie - you simply should be unable to find a term for tha

Types themselves are not proofs. In particular, the proposition associated to a type might be a blatant lie - you simply should be unable to find a term for that type. Also, the notion of blame in a contract maps directly to the type checker telling you which term does not type check.