proposition: Lemma open_te_rec_expr : forall e U k, expr e -> e = open_te_rec k U e.
proof: Proof. intros e U k WF. revert k. induction WF; intros k; simpl; f_equal; auto using open_tt_rec_type; try solve [ unfold open_ee in *; pick fresh x; eapply open_te_rec_expr_aux with (j := 0) (u := exp_fvar x); auto | unfold open_te in *; pick fresh X; eapply open_te_rec_type_aux with (j := 0) (Q := typ_fvar X); auto ]. Qed.
imports: Fsub.Fsub_LetSum_Definitions