proposition: Lemma wf_typ_from_binds_typ : forall x U E, wf_env E -> binds x (bind_typ U) E -> wf_typ E U.
proof: Proof. Proof with auto using wf_typ_weaken_head. induction 1; intros J; analyze_binds J... injection BindsTacVal; intros; subst... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure