proposition: Lemma codePAcorrect2 (f : Formula): ~ mem Formula PA f -> codePA (codeFormula f) = false.
proof: Proof. intros H ; assert (H0: forall x : bool, x = true \/ x = false). { intros x; destruct x; auto. } induction (H0 (codePA (codeFormula f))) as [H1 | H1]. - elim H; apply codePAcorrect1; assumption. - assumption. Qed.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815) hydras.Ackermann(PA codeSubFormula)