proposition: Lemma eSub_eAlgebra: eSub → eAlgebra.
proof: Proof. Proof with intuition. intros [proper closed]. constructor. unfold abstract_algebra.Setoid. apply _. intro o. generalize (closed o). clear closed. unfold algebra_op. simpl. unfold ua_products.product_ops. intro. change (lifted_e _ (algebra_op o) (algebra_op o)). set (f := λ _: bool, algebra_op o) in *. assert (∀ b, lifted_normal _ (f b) (f b)). intros. subst f. simpl. apply algebra_propers... change (lifted_e (σ o) (f true) (f false)). clearbody f. induction (σ o)... simpl in *. repeat intro. unfold respectful in H0. apply (IHo0 (λ b, f b (if b then x else y)))... 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