proposition: Lemma red_regular : forall e e', red e e' -> expr e /\ expr e'.
proof: Proof. Proof with try solve [auto | intuition auto]. intros e e' H. induction H; assert(J := value_regular); split... Case "red_abs". inversion H. pick fresh y. rewrite (subst_ee_intro y)... Case "red_tabs". inversion H. pick fresh Y. rewrite (subst_te_intro Y)... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure