proposition: Lemma insert_cofixed :forall x ys, insert x ys (=) if Z_le_dec (hd ys) x then Cons (hd ys) (insert x (tl ys)) else Cons x ys.
proof: Proof. intros x ys; assert (hyp_bis:=commutativity_Primitive_Corecursion_Cons coalgebra_insert (x,ys)); match goal with | [ id1 : ?X1 (=) ?X2 |- _ ] => apply trans_bisimilar with X2 end; [ assumption | destruct ys as [y ys']; simpl; destruct (Z_le_dec y x); apply refl_bisimilar ]. Qed.
imports: IntensionalLambdaBisimulation ZStreamCoalgebra ZArith