proposition: Lemma tr_int : forall v E V, E |- v ~: V -> forall s, valid E s -> int V (subs s v).
proof: Proof. ind_size1 v; intros E V ht s hs; inversion ht; subst. apply hs. hyp. apply comp_fun. simpl. gen (hu _ _ H2 _ hs); intro h1. simpl in h1. apply h1. eapply hv. apply H4. hyp. try rename X into X0. rename X0 into A; rename V0 into V. simpl. set (x' := var x v s). set (s' := S.update x (Var x') s). gen (cp_int A). intros [A1 A2 A3 A4]. gen (cp_int V). intros [V1 V2 V3 V4]. apply cp_lam; class. intros a ha. unfold s', x'. rewrite subs_comp, single_update_var. eapply hu. refl. apply H3. intros z B. env. rewrite add_mapsto_iff. intros [[h1 h2]|[h1 h2]]; subst. rewrite update_eq. hyp. rewrite update_neq. apply hs. hyp. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)