proposition: Lemma coconstructor_destructor: forall x, coconstructor (w.(transition) x) (=) x.
proof: Proof. intros x. generalize (commutativity_F_unfold (Build_F_coalgebra (F_ w.(states)) (lift_F_ _ _ w.(transition)))). simpl in *; fold coconstructor. intros hyp_cocon. apply (F_unique w (fun x=>coconstructor (w.(transition) x)) (fun x=>x)); intros x0. rewrite (hyp_cocon (w.(transition) x0)); rewrite lift_F_compose; trivial. apply lift_F_id. Qed.
imports: Bisimulation