proposition: Lemma only_even_compute : only_even 8 = 1.
proof: Proof. Proof using. rewrite (@only_even_fix many_steps); [ | apply even_8 ]. { reflexivity. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat