proposition: Lemma subst_te_open_te_var : forall (X Y:atom) U e, Y <> X -> type U -> open_te (subst_te X U e) Y = subst_te X U (open_te e Y).
proof: Proof. Proof with congruence || auto. intros X Y U e Neq WU. unfold open_te. rewrite subst_te_open_te_rec... simpl. destruct (Y == X)... Qed.
imports: Fsub.Fsub_LetSum_Definitions