proposition: Lemma typing_regular : forall E e T, typing E e T -> wf_env E /\ expr e /\ wf_typ E T.
proof: Proof. Proof with simpl_env; try solve [auto | intuition auto]. intros E e T H; induction H... Case "typing_var". repeat split... eauto using wf_typ_from_binds_typ. Case "typing_abs". pick fresh y. destruct (H0 y) as [Hok [J K]]... repeat split. inversion Hok... SCase "Second of original three conjuncts". pick fresh x and apply expr_abs. eauto using type_from_wf_typ, wf_typ_from_wf_env_typ. destruct (H0 x)... SCase "Third of original three conjuncts". apply wf_typ_arrow; eauto using wf_typ_from_wf_env_typ. rewrite_env (empty ++ E). eapply wf_typ_strengthening; simpl_env; eauto. Case "typing_app". repeat split... destruct IHtyping1 as [_ [_ K]]. inversion K... Case "typing_tabs". pick fresh Y. destruct (H0 Y) as [Hok [J K]]... inversion Hok; subst. repeat split... SCase "Second of original three conjuncts". pick fresh X and apply expr_tabs. eauto using type_from_wf_typ, wf_typ_from_wf_env_sub... destruct (H0 X)... SCase "Third of original three conjuncts". pick fresh Z and apply wf_typ_all... destruct (H0 Z)... Case "typing_tapp". destruct (sub_regular _ _ _ H0) as [R1 [R2 R3]]. repeat split... SCase "Second of original three conjuncts". apply expr_tapp... eauto using type_from_wf_typ. SCase "Third of original three conjuncts". destruct IHtyping as [R1' [R2' R3']]. eapply wf_typ_open; eauto. Case "typing_sub". repeat split... destruct (sub_regular _ _ _ H0)... Case "typing_let". repeat split... SCase "Second of original three conjuncts". pick fresh y and apply expr_let... destruct (H1 y) as [K1 [K2 K3]]... SCase "Third of original three conjuncts". pick fresh y. destruct (H1 y) as [K1 [K2 K3]]... rewrite_env (empty ++ E). eapply wf_typ_strengthening; simpl_env; eauto. Case "typing_case". repeat split... SCase "Second of original three conjuncts". pick fresh x and apply expr_case... destruct (H1 x) as [? [? ?]]... destruct (H3 x) as [? [? ?]]... SCase "Third of original three conjuncts". pick fresh y. destruct (H1 y) as [K1 [K2 K3]]... rewrite_env (empty ++ E). eapply wf_typ_strengthening; simpl_env; eauto. Qed.
imports: Fsub.Fsub_LetSum_Infrastructure