proposition: Lemma wf_typ_narrowing : forall V U T E F X, wf_typ (F ++ X ~ bind_sub V ++ E) T -> wf_typ (F ++ X ~ bind_sub U ++ E) T.
proof: Proof. Proof with simpl_env; eauto. intros V U T E F X Hwf_typ. remember (F ++ X ~ bind_sub V ++ E) as G. generalize dependent F. induction Hwf_typ; intros F Heq; subst... Case "wf_typ_var". analyze_binds H... Case "typ_all". pick fresh Y and apply wf_typ_all... rewrite <- app_assoc. apply H0... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure