proposition: Lemma leq_gen_eq : forall (f:E1) (x y:E), leq_gen f x y -> leq_gen f y x -> x = y.
proof: Proof. ir. cp H; cp H0. uh H; uh H0. nin H; nin H0. ee. assert (inc x (U x0)). uh H4; ee; am. assert (inc y (U x0)). uh H4; ee; am. cp (leq_gen_leq H H6 H5). apply leq_leq_eq with x0. uh H; ee. uh H; ee; uh H; ee; am. am. wr H7; am. Qed.
imports: Arith order