proposition: Lemma subSubFormula (f : Formula) (v1 v2 : nat) (s1 s2 : Term): v1 <> v2 -> ~ In v1 (freeVarT s2) -> forall T : System, SysPrf T (iffH (substF (substF f v1 s1) v2 s2) (substF (substF f v2 s2) v1 (substT s1 v2 s2))).
proof: Proof. intros H H0 T; apply (sysExtend L) with (Empty_set Formula). - intros x H1; destruct H1. - elim f using Formula_depth_ind2; intros. + repeat rewrite (subFormulaEqual L). rewrite subSubTerm; auto. rewrite (subSubTerm t0); auto. apply (iffRefl L). + repeat rewrite (subFormulaRelation L). rewrite subSubTerms; auto. apply (iffRefl L). + repeat rewrite (subFormulaImp L). apply (reduceImp L); auto. + repeat rewrite (subFormulaNot L). apply (reduceNot L); auto. + set (v' := newVar (v1 :: v2 :: freeVarF (forallH v a) ++ freeVarT s1 ++ freeVarT s2)) in *. assert (H2: v' <> v1). { intro H2; elim (newVar1 (v1 :: v2 :: freeVarF (forallH v a) ++ freeVarT s1 ++ freeVarT s2)). fold v' ; simpl; auto. } assert (H3: v' <> v2). { intro H3; elim (newVar1 (v1 :: v2 :: freeVarF (forallH v a) ++ freeVarT s1 ++ freeVarT s2)). fold v'; simpl; auto. } assert (H4: ~ In v' (freeVarF (forallH v a))). { intro H4; elim (newVar1 (v1 :: v2 :: freeVarF (forallH v a) ++ freeVarT s1 ++ freeVarT s2)). fold v' ;simpl; auto with datatypes. } assert (H5: ~ In v' (freeVarT s1)). { intro H5; elim (newVar1 (v1 :: v2 :: freeVarF (forallH v a) ++ freeVarT s1 ++ freeVarT s2)). fold v' ; simpl; repeat right; auto with datatypes. } assert (H6: ~ In v' (freeVarT s2)). { intro H6; elim (newVar1 (v1 :: v2 :: freeVarF (forallH v a) ++ freeVarT s1 ++ freeVarT s2)). fold v' ; simpl; repeat right; auto with datatypes. } apply impE with (iffH (substF (substF (forallH v' (substF a v (var v'))) v1 s1) v2 s2) (substF (substF (forallH v' (substF a v (var v'))) v2 s2) v1 (substT s1 v2 s2))). apply (iffE2 L). * assert (H7: folProof.SysPrf L (Empty_set Formula) (iffH (forallH v a) (forallH v' (substF a v (var v'))))) by (apply rebindForall; auto). repeat first [ apply (reduceIff L) | apply (reduceSub L) | apply (notInFreeVarSys L) ]; auto. * assert (H7: forall (f : Formula) (x v : nat) (s : Term), x <> v -> ~ In x (freeVarT s) -> substF (forallH x f) v s = forallH x (substF f v s)). { intros f0 x v0 s H7; rewrite (subFormulaForall L). destruct (eq_nat_dec x v0) as [e | n0]. - elim H7; auto. - destruct (In_dec eq_nat_dec x (freeVarT s)) as [i | n1]. + intro H8; elim H8; auto. + reflexivity. } repeat rewrite H7; try easy. -- apply (reduceForall L). apply (notInFreeVarSys L). apply H1. apply eqDepth with a. symmetry in |- *. apply subFormulaDepth. apply depthForall. -- intro H8; induction (freeVarSubTerm3 _ _ _ _ _ H8). elim H5; eapply in_remove. apply H9. now apply H6. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(ListExt folProp folProof folLogic subProp folReplace)