proposition: Lemma wf_typ_weakening : forall T E F G, wf_typ (G ++ E) T -> uniq (G ++ F ++ E) -> wf_typ (G ++ F ++ E) T.
proof: Proof. Proof with simpl_env; eauto. intros T E F G Hwf_typ Hk. remember (G ++ E) as F'. generalize dependent G. induction Hwf_typ; intros G Hok Heq; subst... Case "type_all". pick fresh Y and apply wf_typ_all... rewrite <- app_assoc. apply H0... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure