proposition: Lemma closedPA1 : ClosedSystem LNT PA.
proof: Proof. unfold ClosedSystem, PA in |- *. intros v f H. induction H as [x H| x H]. - induction H as [x H| x H]. + induction H as [x H| x H]. * induction H as [x H| x H]. -- induction H as [x H| x H]. ++ induction H as [x H| x H]. ** induction H as (x0, H). induction H as (x1, H). unfold PA7 in H. rewrite H. apply freeVarClosed. ** induction H; auto. ++ induction H; auto. -- induction H; auto. * induction H; auto. + induction H; auto. - induction H; auto. Qed.
imports: Coq(Arith Lia Ensembles Decidable) hydras.Ackermann(folProp subAll folLogic3) hydras.Ackermann(NewNotations)