proposition: Lemma conat_transition_dec_inf:forall (S1:F_coalgebra) (s1:S1.(states)), {star | S1.(transition) s1 = inl _ star} + { s1' | S1.(transition) s1 = inr unit s1'}.
proof: Proof. intros [X_st X_tr] x. simpl in x. generalize (refl_equal (X_tr x)). pattern x at 1. destruct (X_tr x) as [star|x']; intros hyp. left; exists star; trivial. right; exists x'; trivial. Qed.
imports: WeaklyFinalCoalgebra