proposition: Lemma reflect_eqdep_weak_spec: reflect_eqdep -> forall A u v, compare_weak_spec u v (@f A A u v).
proof: Proof. intros. case_eq (f u v); try constructor. intro H'. apply reflect_eqdep_eq in H'. subst. constructor. assumption. Defined.
imports: Coq(Arith NArith List RelationClasses)