proposition: Lemma is_suborder_refl : forall a : E, axioms a -> is_suborder a a.
proof: Proof. ir. uf is_suborder; dj. am. am. uf sub; ir; am. uf mor_axioms; dj. uf inclusion; rw source_create. am. uf inclusion; rw target_create; am. uf inclusion; ap create_strong_axioms. uf Umorphism.property. uf Transformation.axioms; ir; am. uf inclusion; rw ev_create. rw ev_create. rw target_create. ufi inclusion H6. rwi source_create H6. am. ufi inclusion H6; rwi source_create H6. ufi leq H6; ee. am. ufi inclusion H6; rwi source_create H6. ufi leq H6; ee; am. Qed.
imports: universe