fact: Definition caseS' {A} {n : nat} (v : t A (S n)) : forall (P : t A (S n) -> Type) (H : forall h t, P (h :: t)), P v := match v with | h :: t => fun P H => H h t | _ => fun devil => False_rect (@IDProp) devil end.
imports: Arith_base