proposition: Lemma permut0_eq_equiv: forall A B, permut0 eq A B -> permut0 equiv A B.
proof: Proof. intros A B H. assert (H':=permut_impl). assert (H1:= H' term term eq equiv A B); clear H'. apply H1. intros a b H'. rewrite H'. reflexivity. assumption. 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)