proposition: Theorem teq_eins_bad : teq one eins.
proof: Proof. cofix CIH. apply teq_two_one_bad, teq_one_two, CIH. Abort. Lemma teq'_two_one : forall r, (r two zwei : Prop) -> paco2 teq_gen r one eins. Proof. intros; pcofix CIH. pfold. rewrite (tunf_eq one), (tunf_eq eins); simpl. constructor; auto. left; pfold. rewrite (tunf_eq two); simpl. constructor; auto. Qed.
imports: Setoid Program Paco.paco