proposition: Lemma open_tt_rec_type_aux : forall T j V i U, i <> j -> open_tt_rec j V T = open_tt_rec i U (open_tt_rec j V T) -> T = open_tt_rec i U T.
proof: Proof. Proof with congruence || eauto. induction T; intros j V i U Neq H; simpl in *; inversion H; f_equal... Case "typ_bvar". destruct (j === n)... destruct (i === n)... Qed.
imports: Fsub.Fsub_LetSum_Definitions