proposition: Lemma codePAcorrect3 (f : Formula): mem Formula PA f -> codePA (codeFormula f) = true.
proof: Proof. intros H; unfold codePA, orRel, nat_rec, nat_rect. do 6 try induction H. - assert (H0: codeInductionSchema (codeFormula x) = true). + apply codeInductionSchemaCorrect1, H. + rewrite H0; repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity. - destruct H. generalize (codeFormula PA1); intro n. rewrite Nat.eqb_refl. repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity. - generalize (codeFormula PA2); intro n. rewrite Nat.eqb_refl. repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity. - generalize (codeFormula PA3); intros n. rewrite Nat.eqb_refl. repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity. - generalize (codeFormula PA4); intros n. rewrite Nat.eqb_refl. repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity. - generalize (codeFormula PA5); intros n. rewrite Nat.eqb_refl. repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity. - rewrite Nat.eqb_refl. repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity. Qed.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815) hydras.Ackermann(PA codeSubFormula)