proposition: Lemma paZeroOrSucc (t : Term): let nv := newVar (0 :: freeVarT t) in SysPrf PA (t = LNT.Zero \/ exH nv, t = LNT.Succ (v#nv))%nt.
proof: Proof. set (nv := newVar (0 :: freeVarT t)) in *. apply impE with (substF (v#0 = LNT.Zero \/ exH nv, v#0 = LNT.Succ v#nv)%nt 0 t). - rewrite (subFormulaOr LNT), (subFormulaEqual LNT); simpl. apply iffE1, (reduceOr LNT). + apply iffRefl. + rewrite (subFormulaExist LNT). destruct (eq_nat_dec nv 0) as [a | b]. * elim (newVar1 (0 :: freeVarT t)). fold nv in |- *. rewrite a; simpl; auto. * destruct (In_dec eq_nat_dec nv (freeVarT t)) as [a | b0]. -- elim (newVar1 (0 :: freeVarT t)). fold nv in |- *; simpl in |- *; auto. -- rewrite (subFormulaEqual LNT). Opaque eq_nat_dec. simpl in |- *. Transparent eq_nat_dec. destruct (eq_nat_dec 0 nv) as [e | n ]. ++ elim b; auto. ++ apply iffRefl. - apply forallE, induct. + rewrite (subFormulaOr LNT); apply orI1. rewrite (subFormulaEqual LNT); simpl; apply eqRefl. + apply forallI. * apply closedPA. * apply impI; rewrite (subFormulaOr LNT); apply orI2. rewrite (subFormulaExist LNT). induction (eq_nat_dec nv 0). -- elim (newVar1 (0 :: freeVarT t)). fold nv; simpl; auto. -- induction (In_dec eq_nat_dec nv (freeVarT (LNT.Succ (v#0))%nt)) as [a | b0]. ++ elim (newVar1 (0 :: freeVarT t)). fold nv in |- *. simpl in a. induction a as [H| H]. ** simpl in |- *. auto. ** elim H. ++ rewrite (subFormulaEqual LNT). Opaque eq_nat_dec. simpl in |- *. Transparent eq_nat_dec. induction (nat_rec (fun n : nat => {0 = n} + {0 <> n}) (left (0 <> 0) (refl_equal 0)) (fun (m : nat) (_ : {0 = m} + {0 <> m}) => right (0 = S m) (O_S m)) nv) as [a | b1]. ** elim b; auto. ** fold (Succ (var nv)). apply sysWeaken; apply existI with (var 0). rewrite (subFormulaEqual LNT). simpl in |- *. destruct (eq_nat_dec nv 0) as [e | n]. { elim b1; auto. } change match nv as n return ({0 = n} + {0 <> n}) with | 0 => left (0 <> 0) (refl_equal 0) | S m => right (0 = S m) (O_S m) end with (eq_nat_dec 0 nv). destruct (eq_nat_dec 0 nv) as [e | n0]. { now elim b1. } simpl; destruct (eq_nat_dec nv nv) as [? | n1]. { apply eqRefl. } now destruct n1. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(subAll folReplace folProp folLogic3 NN LNN2LNT) hydras.Ackermann(NewNotations)