proposition: Lemma teq'_one_two : forall r, (r one eins : Prop) -> paco2 teq_gen r two zwei.
proof: Proof. intros; pcofix CIH. pfold. rewrite (tunf_eq two), (tunf_eq zwei); simpl. constructor; auto. Qed.
imports: Setoid Program Paco.paco