proposition: Lemma eq_proof : equivalence A eq_A.
proof: Proof. unfold eq_A; split. intro a; reflexivity. intros a1 a2 a3 H1 H2; transitivity a2; trivial. intros a1 a2 H; symmetry; trivial. Qed.
imports: Coq(Relation_Definitions Setoid Bool Arith)