proposition: Lemma rev_induction A (P : list A -> Prop) : P nil -> (forall a l, P l -> P (l ++ a :: nil)) -> forall l, P l.
proof: Proof. ins; rewrite <- rev_involutive. induction (rev l); ins; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation