proposition: Lemma leq_suborder_all : forall a b x y : E, axioms a -> sub b (U a) -> leq (suborder b a) x y = A (inc x b) (A (inc y b) (leq a x y)).
proof: Proof. intros. apply iff_eq; intros. pose (leq_suborder_then H H0 H1). ee; am. apply leq_suborder_if; ee; am. Qed.
imports: universe