proposition: Lemma equiv_term_activeEnv : forall M N, term M = term N -> env M [<->] env N -> activeEnv M = activeEnv N.
proof: Proof. intro M; destruct M as [E Pt T M]; induction M; intro N; term_inv N; intros. inversion H. rewrite (H0 x A A0); trivial. rewrite H2; trivial. fold (activeEnv (buildT T)). rewrite <- (IHM (buildT T)); trivial. inversion H; trivial. simpl; unfold decl. apply env_comp_cons; trivial. left; inversion H; trivial. fold (activeEnv (buildT T1)). fold (activeEnv (buildT T2)). rewrite <- IHM1. rewrite <- IHM2; trivial. inversion H; trivial. inversion H; trivial. trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)