proposition: Lemma eqb_eq : forall t1 t2, eqb t1 t2 = true <-> eq t1 t2.
proof: Proof. intros. unfold eqb; unfold eq. split; intro H. apply andb_true_iff in H. induction H. split; apply Pos.eqb_eq; assumption. induction H. apply andb_true_iff. split; apply Pos.eqb_eq; assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms