proposition: Lemma activeEnv_minimal_len : forall M M', env M [<->] env M' -> term M = term M' -> length (activeEnv M) = length (activeEnv M').
proof: Proof. destruct M as [E Pt T M]; induction M; intros; term_inv M'. inversion H0. autorewrite with datatypes using simpl; trivial. fold (activeEnv (buildT M)) in *; fold (activeEnv (buildT T)). rewrite !length_tail_minus. inversion H0. rewrite (IHM (buildT T)); simpl; trivial. unfold decl; apply env_comp_cons; trivial. left; try_solve. fold (activeEnv (buildT M1)) in *; fold (activeEnv (buildT T1)). fold (activeEnv (buildT M2)) in *; fold (activeEnv (buildT T2)). rewrite !env_sum_length. inversion H0. rewrite (IHM1 (buildT T1)); trivial. rewrite (IHM2 (buildT T2)); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)