proposition: Lemma equal_eq : forall a b, equal a b = true -> a = b.
proof: Proof. intros. apply eq_equal in H. destruct a as (a, asort, anodef), b as (b, bsort, bnodef). unfold eq in H. revert b bsort bnodef H. induction a; intros; destruct b. rewrite (proof_irrelevance _ asort bsort). rewrite (proof_irrelevance _ anodef bnodef). auto. simpl in H. now contradict H. simpl in H. destruct a; now contradict H. simpl in H. destruct a, p. destruct (compare k k0); auto; try (now contradict H). destruct H. subst. inversion_clear asort. inversion_clear bsort. specialize (nodefault_tail bnodef). specialize (nodefault_tail anodef). intros. specialize (IHa H H4 b H2 H5 H0). inversion IHa. subst. rewrite (proof_irrelevance _ asort bsort). rewrite (proof_irrelevance _ anodef bnodef). reflexivity. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance