proposition: Lemma commutativity_Corecursor_rel_image_lifting (BT: BT_coalgebroid) (x:BT.(bs_states)) : rel_image_lift_B_ w w bisimilar (w.(transition) (Corecursor BT x)) (lift_B_ _ _ (prim_corec_tupling _ (Corecursor BT)) (BT.(bs_transition) x)).
proof: Proof. apply MB_Weakly_Final_Coalgebra_Theory.rel_image_bisimilar_transitive with (lift_B_ _ _ (fun x0=> Beta prim_corec_distributive (lift_T_ _ _ (Corecursor BT) x0)) (bs_transition BT x)). generalize (commutativity_Lam_coiterator_rel_image_lifting prim_corec_distributive BT x). fold Corecursor; rewrite lift_B_compose; trivial. apply lift_B_extensionality_bisim. clear; intros x. rewrite Beta_corecursor_cotupling_id. destruct x as [x0 | w0]; simpl. unfold identity_as_Set_Functor.lift_F_; apply MB_Weakly_Final_Coalgebra_Theory.refl_bisimilar. unfold Weak_fin_coalg_as_Set_Functor.lift_F_; apply MB_Weakly_Final_Coalgebra_Theory.refl_bisimilar. Qed.
imports: WeaklyFinalCoalgebra