proposition: Lemma activeEnv_var_decl : forall M x A, term M = %x -> env M |= x := A -> activeEnv M |= x := A.
proof: Proof. intro M; term_inv M; intros. inversion H. replace A with A0. unfold VarD, EmptyEnv, decl; apply nth_after_copy. rewrite <- H2 in H0. inversion T; inversion H0; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)