proposition: Lemma oppreserving_inc_subalgebra {w : SymbolType σ} (α : Operation A w) (C : ClosedUnderOp A P α) : OpPreserving def_inc_subalgebra (op_subalgebra A P α C) α.
proof: Proof. induction w. - reflexivity. - intros x. apply IHw. Defined.
imports: HoTT.HProp HoTT.Types HoTT.Classes.theory.ua_homomorphism