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