proposition: Theorem park_principle (A:Type) (R:LList A -> LList A -> Prop) : bisimulation R -> forall l1 l2:LList A, R l1 l2 -> bisimilar l1 l2.
proof: Proof. intros bisim; cofix H. intros l1 l2; case l1; case l2. - left. - intros a l H0; generalize (bisim _ _ H0). intro H1; discriminate H1. - intros a l H0; generalize (bisim _ _ H0). contradiction. - intros a l a0 l0 H0; generalize (bisim _ _ H0). intros [e1 H1]; subst a0; right; now apply H. Qed.
imports: Arith List RelationClasses