proposition: Lemma open_te_rec_expr_aux : forall e j u i P , open_ee_rec j u e = open_te_rec i P (open_ee_rec j u e) -> e = open_te_rec i P e.
proof: Proof. Proof with congruence || eauto. induction e; intros j u i P H; simpl in *; inversion H; f_equal... Qed.
imports: Fsub.Fsub_LetSum_Definitions