proposition: Lemma eqone'_eins: eqone' eins.
proof: Proof. pcofix CIH0; pfold. rewrite (tunf_eq eins); simpl. constructor; [right; apply CIH0|]. left; pcofix CIH1; pfold. constructor; [right; apply CIH0|]. rewrite (tunf_eq zwei). right; apply CIH1. Qed.
imports: Setoid Program Paco.paco