proposition: Lemma eqone_eins : eqone eins.
proof: Proof. cofix CIH0. rewrite (tunf_eq eins); simpl. constructor; [apply CIH0|]. cofix CIH1. constructor; [apply CIH0|]. rewrite (tunf_eq zwei). apply CIH1. Qed.
imports: Setoid Program Paco.paco