proposition: Lemma subst_ee_open_ee_var : forall (x y:atom) u e, y <> x -> expr u -> open_ee (subst_ee x u e) y = subst_ee x u (open_ee e y).
proof: Proof. Proof with congruence || auto. intros x y u e Neq Wu. unfold open_ee. rewrite subst_ee_open_ee_rec... simpl. destruct (y == x)... Qed.
imports: Fsub.Fsub_LetSum_Definitions