proposition: Lemma open_ee_rec_expr_aux : forall e j v u i, i <> j -> open_ee_rec j v e = open_ee_rec i u (open_ee_rec j v e) -> e = open_ee_rec i u e.
proof: Proof. Proof with congruence || eauto. induction e; intros j v u i Neq H; simpl in *; inversion H; f_equal... Case "exp_bvar". destruct (j===n)... destruct (i===n)... Qed.
imports: Fsub.Fsub_LetSum_Definitions