proposition: Lemma eAlgebra_eSub: eAlgebra → eSub.
proof: Proof. Proof with intuition. intros. constructor. unfold Q. repeat intro. constructor; intro. rewrite <- (H1 true), <- (H1 false)... rewrite (H1 true), (H1 false)... intro o. simpl. unfold algebra_op, ua_products.product_ops, algebra_op. set (f := λ _: bool, vo o). assert (∀ b, Proper (=) (f b)). intro. unfold f. apply algebra_propers. assert (lifted_e _ (f true) (f false)). unfold f. unfold lifted_e. destruct H0. apply algebra_propers. assert (∀ b, Proper (lifted_e (σ o)) (f b))... clearbody f. induction (σ o)... simpl in *... apply IHo0... apply H1... 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