proposition: Lemma tr_subs : forall E v V, E |- v ~: V -> forall s F, F |-s s ~: E -> F |- subs s v ~: V.
proof: Proof. cut (forall E v V, E |- v ~: V -> forall s F, F |-s s ~: restrict_dom E (fv v) -> F |- subs s v ~: V). intros h E v V ht s F hs. eapply h. apply ht. intros x T. rewrite mapsto_restrict_dom. intros [h1 h2]. apply hs. hyp. induction 1; simpl; intros s F hs. apply hs. rewrite mapsto_restrict_dom. set_iff. tauto. apply tr_fun. apply tr_app with V. apply IHtr1. intros x A. rewrite mapsto_restrict_dom. intros [h1 h2]. apply hs. rewrite mapsto_restrict_dom. set_iff. tauto. apply IHtr2. intros x A. rewrite mapsto_restrict_dom. intros [h1 h2]. apply hs. rewrite mapsto_restrict_dom. set_iff. tauto. set (x' := var x v s). set (s' := S.update x (Var x') s). apply tr_lam. apply IHtr. intros y T. env. rewrite mapsto_restrict_dom, add_mapsto_iff. intros [[[h1 h2]|[h1 h2]] h3]; unfold s', Def.update; eq_dec y x. subst y T. apply tr_var. env. rewrite add_mapsto_iff. intuition. intuition. intuition. assert (h2' : MapsTo y T (restrict_dom E (XSet.remove x (fv v)))). rewrite mapsto_restrict_dom. set_iff. intuition. gen (hs _ _ h2'); intro h. apply tr_restrict in h. set (F' := restrict_dom F (fv (s y))) in h. case_eq (find x' F'). intro U'. rewrite <- find_mapsto_iff. unfold F'. rewrite mapsto_restrict_dom. intros [i1 i2]. exfalso. eapply var_notin_fv_subs. apply h3. apply n. apply i2. intro i. eapply tr_le with (x:=add x' _ F'); try refl. unfold F'. rewrite restrict_dom_le. refl. rewrite <- le_add; hyp. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)