proposition: Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n.
proof: Proof. intros m n p; revert n; induction p as [|? p IHp]; intros ? q; destruct q; simpl; intros; f_equal. - now apply Nat.eqb_eq. - easy. - easy. - eapply IHp. eassumption. Qed.
imports: PeanoNat