proposition: Lemma eqb_eq : forall n (p q : t n), eqb p q = true <-> p = q.
proof: Proof. apply rect2; simpl; intros. - split; intros ; [ reflexivity | now apply Nat.eqb_eq ]. - now split. - now split. - eapply iff_trans. + eassumption. + split. * intros; now f_equal. * apply FS_inj. Qed.
imports: PeanoNat