proposition: Lemma wf_typ_subst_tb : forall F Q E Z P T, wf_typ (F ++ Z ~ bind_sub Q ++ E) T -> wf_typ E P -> uniq (map (subst_tb Z P) F ++ E) -> wf_typ (map (subst_tb Z P) F ++ E) (subst_tt Z P T).
proof: Proof. Proof with simpl_env; eauto using wf_typ_weaken_head, type_from_wf_typ. intros F Q E Z P T WT WP. remember (F ++ Z ~ bind_sub Q ++ E) as G. generalize dependent F. induction WT; intros F EQ Ok; subst; simpl subst_tt... Case "wf_typ_var". destruct (X == Z); subst... SCase "X <> Z". analyze_binds H... apply (wf_typ_var (subst_tt Z P U))... Case "wf_typ_all". pick fresh Y and apply wf_typ_all... rewrite subst_tt_open_tt_var... rewrite_env (map (subst_tb Z P) (Y ~ bind_sub T1 ++ F) ++ E). apply H0... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure