fact: Definition caseS' {n : nat} (p : t (S n)) : forall (P : t (S n) -> Type) (P1 : P F1) (PS : forall (p : t n), P (FS p)), P p := match p with | @F1 k => fun P P1 PS => P1 | FS pp => fun P P1 PS => PS pp end.
imports: PeanoNat