proposition: Lemma map_subst_tb_id : forall G Z P, wf_env G -> Z `notin` dom G -> G = map (subst_tb Z P) G.
proof: Proof. Proof with auto. intros G Z P H. induction H; simpl; intros Fr; simpl_env... rewrite <- IHwf_env... rewrite <- subst_tt_fresh... eapply notin_fv_wf; eauto. rewrite <- IHwf_env... rewrite <- subst_tt_fresh... eapply notin_fv_wf; eauto. Qed.
imports: Fsub.Fsub_LetSum_Infrastructure