proposition: Lemma activeEnv_length : forall M, length (activeEnv M) <= length (env M).
proof: Proof. destruct M as [E Pt T M]; induction M. simpl; autorewrite with datatypes using simpl. assert (x < length E); [idtac | lia]. apply (proj1 (nth_in E x)). inversion v; try_solve. simpl; lia. simpl; fold (activeEnv (buildT M)). destruct (activeEnv (buildT M)). simpl; lia. simpl in *; lia. simpl; fold (activeEnv (buildT M1)); fold (activeEnv (buildT M2)). rewrite env_sum_length. apply Nat.max_case; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)