proposition: Lemma subAllFormulaId (T : fol.System L) (f : fol.Formula L): folProof.SysPrf L T (iffH (subAllFormula f (fun x : nat => var x)) f).
proof: Proof. apply (sysExtend L) with (Empty_set (fol.Formula L)). - intros x H; contradiction H. - induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl. + repeat rewrite subAllTermId; apply (iffRefl L). + rewrite subAllTermsId; apply (iffRefl L). + apply (reduceImp L). * apply Hrecf1. * apply Hrecf0. + apply (reduceNot L). apply Hrecf. + set (nv := newVar (freeVarF f ++ freeVarMap (List.remove eq_nat_dec n (freeVarF f)) (fun x : nat => var x))). apply (iffTrans L) with (forallH n (subAllFormula f (fun x : nat => var x))). * apply (iffTrans L) with (forallH nv (substF (subAllFormula f (fun x : nat => var x)) n (var nv))). -- replace (subAllFormula f (fun v : nat => match eq_nat_dec v n with | left _ => var nv | right _ => var v end)) with (subAllFormula f (fun x : nat => substT (var x) n (var nv))). ++ apply (reduceForall L). ** apply (notInFreeVarSys L). ** apply (iffSym L). apply subSubAllFormula with (m := fun x : nat => var x). ++ apply subAllFormula_ext. intros m H; simpl. induction (eq_nat_dec n m); induction (eq_nat_dec m n); reflexivity || (assert False by auto; contradiction). -- apply (iffSym L). apply (rebindForall L). intro H; assert (H0: In nv (freeVarF (subAllFormula f (fun x : nat => var x)))) by (eapply in_remove; apply H). decompose record (freeVarSubAllFormula1 _ _ _ H0) /r; intros x H2 H3. elim (newVar1 (freeVarF f ++ freeVarMap (List.remove eq_nat_dec n (freeVarF f)) (fun x : nat => var x))). fold nv; apply in_or_app; right. eapply freeVarMap1. ++ apply H3. ++ apply in_in_remove. ** destruct H3 as [H1| H1]. --- rewrite H1. eapply in_remove_neq. apply H. --- contradiction. ** apply H2. * apply (reduceForall L). -- apply (notInFreeVarSys L). -- apply Hrecf. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)