proposition: Lemma open_ee_rec_expr : forall u e k, expr e -> e = open_ee_rec k u e.
proof: Proof. Proof with auto. intros u e k Hexpr. revert k. induction Hexpr; intro k; simpl; f_equal; auto*; try solve [ unfold open_ee in *; pick fresh x; eapply open_ee_rec_expr_aux with (j := 0) (v := exp_fvar x); auto | unfold open_te in *; pick fresh X; eapply open_ee_rec_type_aux with (j := 0) (V := typ_fvar X); auto ]. Qed.
imports: Fsub.Fsub_LetSum_Definitions