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