proposition: Lemma rel_image_bisimilar_transitive: forall fw1 fw2 fw3, rel_image_lift_F_ _ _ bisimilar fw1 fw2 -> rel_image_lift_F_ _ _ bisimilar fw2 fw3 -> rel_image_lift_F_ _ _ bisimilar fw1 fw3.
proof: Proof. intros fs1 fs2 fs3 (x1 & y1 & hyp11 & hyp12 & hyp13) (x2 & y2 & hyp21 & hyp22 & hyp23). red. exists x1; exists y2. repeat split; trivial. rewrite hyp11. rewrite <- hyp21. symmetry. apply destructor_equal_inversion. rewrite <- hyp13. rewrite <- hyp22; trivial. Qed.
imports: Bisimulation