proposition: Lemma leq_gen_def1 : forall (f:E1) (x y:E), leq_gen f x y -> leq_gen f x x.
proof: Proof. ir. uh H; nin H. ee. assert (inc x (U x0)). uh H0; ee; am. cp (leq_gen_leq H H1 H1). rw H2. apply leq_refl. uh H; ee; uh H; ee; uh H; ee; am. am. Qed.
imports: Arith order