proposition: Lemma activeEnv_var_single : forall M x y A, term M = %x -> activeEnv M |= y := A -> x = y.
proof: Proof. intros. destruct (activeEnv_var_det M H H0); auto. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)