fact: Fixpoint to_nat {m} (n : t m) : {i | i < m} := match n with |@F1 j => exist _ 0 (Nat.lt_0_succ j) |FS p => match to_nat p with |exist _ i P => exist _ (S i) (proj1 (Nat.succ_lt_mono _ _) P) end end.
imports: PeanoNat