fact: Definition rel_image_lift_F_ (S1 S2:F_coalgebra) (R:S1.(states) -> S2.(states) -> Prop) (b_x : F_ (states S1)) (b_y : F_ (states S2)) : Prop := exists x : states S1, exists y : states S2, R x y /\ b_x = transition S1 x /\ b_y = transition S2 y.
imports: ExtensionalFunctor Setoid