[isabelle] A::pcpo , datatype B = Cons A . Is B::pcpo?



Hello,
is there an elegant way to show that B is also a PCPO? (since Cons is bijective)

Thank you!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.