proposition: Lemma equiv_same_length : forall f1 f2 l1 l2, equiv (Term f1 l1) (Term f2 l2) -> length l1 = length l2.
proof: Proof. intros f1 f2 l1 l2 t1_eq_t2. inversion t1_eq_t2. trivial. apply equiv_list_lex_same_length; assumption. apply (@permut_length _ equiv); trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)