proposition: Lemma rev_ind_type : forall P : Multiset -> Type, P nil -> (forall x l, P l -> P (l ++ x :: nil)) -> forall l, P l.
proof: Proof. intros. gen (rev_involutive l). intros E; rewrite <- E. apply (rev_list_ind_type P). auto. simpl in |- *. intros. apply (X0 a (rev l0)). auto. Defined.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)