proposition: Theorem teq_one : teq one eins.
proof: Proof. cofix CIH. apply teq_fold. rewrite (tunf_eq one), (tunf_eq eins); simpl. constructor; auto. apply teq_fold. rewrite (tunf_eq two); simpl. constructor; auto. cofix CIH'. apply teq_fold. rewrite (tunf_eq two), (tunf_eq zwei); simpl. constructor; auto. Qed.
imports: Setoid Program Paco.paco