proposition: Lemma subst_tt_open_tt_var : forall (X Y:atom) P T, Y <> X -> type P -> open_tt (subst_tt X P T) Y = subst_tt X P (open_tt T Y).
proof: Proof. Proof with congruence || auto. intros X Y P T Neq Wu. unfold open_tt. rewrite subst_tt_open_tt_rec... simpl. destruct (Y == X)... Qed.
imports: Fsub.Fsub_LetSum_Definitions