fact: Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs)) ls : P ls := match ls with | nil => N | x::xs => C x xs end.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality