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