proposition: Lemma membersOk n : n = codeList (members n).
proof: Proof. pattern n, (members n); apply members_elim. - reflexivity. - intros; simpl; f_equal; rewrite <- H. now rewrite cPairProjections. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith) Equations(Equations)