proposition: Lemma open_ee_rec_type_aux : forall e j V u i, open_te_rec j V e = open_ee_rec i u (open_te_rec j V e) -> e = open_ee_rec i u e.
proof: Proof. induction e; intros j V u i H; simpl; inversion H; f_equal; eauto. Qed.
imports: Fsub.Fsub_LetSum_Definitions