proposition: Lemma reduceSubAll : forall (T : fol.System L) (map : nat -> fol.Term L) (A B : fol.Formula L), (forall v : nat, ~ In_freeVarSys L v T) -> folProof.SysPrf L T (iffH A B) -> folProof.SysPrf L T (iffH (subAllFormula A map) (subAllFormula B map)).
proof: Proof. assert (H: forall (T : fol.System L) (map : nat -> fol.Term L) (A B : fol.Formula L), (forall v : nat, ~ In_freeVarSys L v T) -> folProof.SysPrf L T (iffH A B) -> folProof.SysPrf L T (impH (subAllFormula A map) (subAllFormula B map))). { intros T map A B H H0; replace (impH (subAllFormula A map) (subAllFormula B map)) with (subAllFormula (impH A B) map). - set (n := newVar (freeVarF (impH A B))). replace (subAllFormula (impH A B) map) with (subAllFormula (impH A B) (fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => map x end)). + apply subAllCloseFrom. induction n as [| n Hrecn]. * simpl; apply (iffE1 L), H0. * simpl; apply (forallI L). -- apply H. -- apply Hrecn. + apply subAllFormula_ext. intros m H1; induction (le_lt_dec n m) as [a | ?]. * rewrite Nat.le_ngt in a; destruct a. unfold n; now apply newVar2. * auto. - reflexivity. } intros T map A B H0 H1; apply (iffI L). - apply H; auto. - apply H; auto. now apply (iffSym L). Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)