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), b as (b, bsort). unfold eq in H. revert b bsort H. induction a; intros; destruct b. apply f_equal. apply proof_irrelevance. 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 (IHa H b H2 H0). inversion IHa. subst. apply f_equal. apply proof_irrelevance. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses ProofIrrelevance