proposition: Lemma suborder_inclusion_mor_axioms : forall a b : E, axioms a -> sub b (U a) -> mor_axioms (suborder_inclusion b a).
proof: Proof. intros. unfold suborder_inclusion in |- *. unfold mor_axioms in |- *; ee. unfold inclusion in |- *; rewrite source_create. apply suborder_axioms; au. unfold inclusion in |- *; rewrite target_create. am. unfold inclusion in |- *. apply create_strong_axioms. unfold Umorphism.property in |- *. unfold Transformation.axioms in |- *. intros. rewrite underlying_suborder in H1. apply H0; au. intros. unfold inclusion in |- *. rewrite target_create. repeat rewrite ev_create. unfold inclusion in H1; rewrite source_create in H1. rewrite leq_suborder_all in H1. ee. am. am. am. unfold inclusion in H1; rewrite source_create in H1. rewrite leq_suborder_all in H1; au. ee. rewrite underlying_suborder; am. unfold inclusion in H1; rewrite source_create in H1. rewrite leq_suborder_all in H1; au. ee. rewrite underlying_suborder; au. Qed.
imports: universe