proposition: Lemma subst_ee_intro_rec : forall x e u k, x `notin` fv_ee e -> open_ee_rec k u e = subst_ee x u (open_ee_rec k (exp_fvar x) e).
proof: Proof. Proof with congruence || auto. induction e; intros u k Fr; simpl in *; f_equal... Case "exp_bvar". destruct (k === n)... simpl. destruct (x == x)... Case "exp_fvar". destruct (a == x)... contradict Fr; fsetdec. Qed.
imports: Fsub.Fsub_LetSum_Definitions