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