proposition: Lemma typing_narrowing : forall Q E F X P e T, sub E P Q -> typing (F ++ X ~ bind_sub Q ++ E) e T -> typing (F ++ X ~ bind_sub P ++ E) e T.
proof: Proof. Proof with eauto 6 using wf_env_narrowing, wf_typ_narrowing, sub_narrowing. intros Q E F X P e T PsubQ Typ. remember (F ++ X ~ bind_sub Q ++ E) as E'. generalize dependent F. induction Typ; intros F EQ; subst... Case "typing_var". analyze_binds H0... Case "typing_abs". pick fresh y and apply typing_abs. rewrite <- app_assoc. apply H0... Case "typing_tabs". pick fresh Y and apply typing_tabs. rewrite <- app_assoc. apply H0... Case "typing_let". pick fresh y and apply typing_let... rewrite <- app_assoc. apply H0... Case "typing_case". pick fresh y and apply typing_case... SCase "inl branch". rewrite <- app_assoc. apply H0... SCase "inr branch". rewrite <- app_assoc. apply H2... Qed.
imports: Fsub.Fsub_LetSum_Lemmas