proposition: Lemma sub_regular : forall E S T, sub E S T -> wf_env E /\ wf_typ E S /\ wf_typ E T.
proof: Proof. Proof with simpl_env; try solve [auto | intuition auto]. intros E S T H. induction H... Case "sub_trans_tvar". intuition eauto. Case "sub_all". repeat split... SCase "Second of original three conjuncts". pick fresh Y and apply wf_typ_all... destruct (H1 Y)... rewrite_env (empty ++ Y ~ bind_sub S1 ++ E). apply (wf_typ_narrowing T1)... SCase "Third of original three conjuncts". pick fresh Y and apply wf_typ_all... destruct (H1 Y)... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure