proposition: Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
proof: Proof. induction p as [|? p IHp]. - reflexivity. - simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p). Qed.
imports: PeanoNat