Library hydras.solutions_exercises.OnCodeList

From hydras.Ackermann Require Import primRec cPair.
From Coq Require Import Arith.
From Equations Require Import Equations.

Equations members (a:nat): list nat by wf a:=
  members 0 := List.nil;
  members (S z) := cPairPi1 z:: members (cPairPi2 z).

Lemma membersOk n : n = codeList (members n).

Lemma membersOk' l : l = members (codeList l).