proposition: Lemma subToSubAll (T : fol.System L) (A : fol.Formula L) (v : nat) (s : fol.Term L): folProof.SysPrf L T (iffH (substF A v s) (subAllFormula A (fun x : nat => match eq_nat_dec v x with | left _ => s | right _ => var x end))).
proof: Proof. apply (iffTrans L) with (substF (subAllFormula A (fun x : nat => var x)) v s). apply sysExtend with (Empty_set (fol.Formula L)). - intros x H; contradiction H. - apply (reduceSub L). intros [x [H H0]]; induction H0. apply (iffSym L), subAllFormulaId. - eapply (iffTrans L). + apply subSubAllFormula. + replace (subAllFormula A (fun x : nat => match eq_nat_dec v x with | left _ => s | right _ => var x end)) with (subAllFormula A (fun n : nat => substT ((fun x : nat => var x) n) v s)). * apply (iffRefl L). * apply subAllFormula_ext; intros m H; now simpl. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)