proposition: Lemma prod_eq_spec : forall x y, if prod_eq x y then x = y else x <> y.
proof: Proof. intros (x1,x2) (y1,y2); simpl;generalize (Aeq_spec x1 y1);destruct (Aeq x1 y1);intros;subst. generalize (Beq_spec x2 y2);destruct (Beq x2 y2);intros;subst;trivial. intro H1;injection H1;auto. intro H1;injection H1;auto. Qed.
imports: Coq(List)