proposition: Lemma square o0 x x' y y': Preservation σ A B f x x' → Preservation σ A B f y y' → op_type_equiv (sorts σ) B o0 x' y' → @op_type_equiv (sorts σ) A (λ s: sorts σ, @in_domain (A s) (B s) (e0 s) (f s)) o0 x y.
proof: Proof. induction o0. simpl. intros. unfold in_domain. rewrite H3, H4. assumption. simpl in *. repeat intro. unfold in_domain in H6. unfold respectful in H5. simpl in *. pose proof (H3 x0). pose proof (H3 y0). clear H3. pose proof (H4 x0). pose proof (H4 y0). clear H4. apply (IHo0 (x x0) (x' (f _ x0)) (y y0) (y' (f _ y0)) H7 H9). apply H5. assumption. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util