proposition: Lemma membersOk' l : l = members (codeList l).
proof: Proof. induction l. - reflexivity. - cbn; rewrite IHl. rewrite members_equation_2. now rewrite cPairProjections1, cPairProjections2, <- !IHl. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith) Equations(Equations)