proposition: Lemma open_te_rec_type_aux : forall e j Q i P, i <> j -> open_te_rec j Q e = open_te_rec i P (open_te_rec j Q e) -> e = open_te_rec i P e.
proof: Proof. induction e; intros j Q i P Neq Heq; simpl in *; inversion Heq; f_equal; eauto using open_tt_rec_type_aux. Qed.
imports: Fsub.Fsub_LetSum_Definitions