proposition: Theorem teq'_two : teq' two zwei.
proof: Proof. pcofix CIH. pfold. rewrite (tunf_eq two), (tunf_eq zwei); simpl. constructor; auto. left; 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