proposition: Lemma destructor_morphism : forall x y, x(=)y -> maximal_bisimulation (Build_F_coalgebra (F_ w.(states)) (lift_F_ _ _ w.(transition))) (Build_F_coalgebra (F_ w.(states)) (lift_F_ _ _ w.(transition))) (w.(transition) x) (w.(transition) y).
proof: Proof. intros x y hyp. apply F_unfold_morphism_inversion. fold coconstructor. do 2 rewrite coconstructor_destructor; trivial. Qed.
imports: Bisimulation