proposition: Lemma conv_env_var: forall M N x y Q, envSub Q x y -> term M = %x -> term N = %y -> type M = type N -> conv_env M N Q.
proof: Proof. intros; intros p q pq B. split; intro D. destruct (activeEnv_var_det M H0 D). rewrite H3 in pq. rewrite <- (envSub_Lok Q x y q H pq). rewrite (activeEnv_var N H1). rewrite <- H2; rewrite H4. unfold VarD, decl, EmptyEnv; apply nth_after_copy. destruct (activeEnv_var_det N H1 D). rewrite H3 in pq. rewrite <- (envSub_Rok Q x p y H pq). rewrite (activeEnv_var M H0). rewrite H2; rewrite H4. unfold VarD, decl, EmptyEnv; apply nth_after_copy. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)