proposition: Lemma codeInductionSchemaCorrect1 (f : Formula) : InductionSchema f -> codeInductionSchema (codeFormula f) = true.
proof: Proof. intros [x [x0 H]]; unfold PA7 in H; rewrite H; clear H f. lazy beta delta [codeInductionSchema] in |- *. rewrite codeOpenCorrect; replace (open (close LNT (impH (substF x x0 Zero) (impH (forallH x0 (impH x (substF x x0 (Succ (var x0))))) (forallH x0 x))))) with (impH (substF x x0 Zero) (impH (forallH x0 (impH x (substF x x0 (Succ (var x0))))) (forallH x0 x))). - replace (cadr (cddddr (codeFormula (impH (substF x x0 Zero) (impH (forallH x0 (impH x (substF x x0 (Succ (var x0))))) (forallH x0 x)))))) with x0. + replace (cddr (cddddr (codeFormula (impH (substF x x0 Zero) (impH (forallH x0 (impH x (substF x x0 (Succ (var x0))))) (forallH x0 x)))))) with (codeFormula x). * cbv zeta; unfold codeFormula; rewrite <- codeCloseCorrect. replace (codeClose (codeImp (codeSubFormula (code.codeFormula x) x0 (codeTerm Zero)) (codeImp (codeForall x0 (codeImp (code.codeFormula x) (codeSubFormula (code.codeFormula x) x0 (codeTerm (Succ (var x0)))))) (codeForall x0 (code.codeFormula x))))) with (codeClose (code.codeFormula (impH (substF x x0 Zero) (impH (forallH x0 (impH x (substF x x0 (Succ (var x0))))) (forallH x0 x))))). -- rewrite Nat.eqb_refl; reflexivity. -- simpl; unfold codeTerm; repeat rewrite codeSubFormulaCorrect. reflexivity. * simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. + simpl in |- *. repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. - unfold close. induction (List.nodup Nat.eq_dec (freeVarF (impH (substF x x0 Zero) (impH (forallH x0 (impH x (substF x x0 (Succ (var x0))))) (forallH x0 x))))). + reflexivity. + simpl; assumption. Qed.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815) hydras.Ackermann(PA codeSubFormula)