fact: Fixpoint Preservation {n : OpType}: op_type A n → op_type B n → Prop := match n with | ne_list.one d => λ oA oB, f oA = oB | ne_list.cons x y => λ oA oB, ∀ x, Preservation (oA x) (oB (f x)) end.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra