proposition: Lemma subWithEquals : forall (f : fol.Formula L) (v : nat) (a b : fol.Term L) (T : fol.System L), SysPrf T (a = b)%fol -> SysPrf T (substF f v a -> substF f v b)%fol.
proof: Proof. intro f; elim f using Formula_depth_ind2; intros. - repeat rewrite subFormulaEqual. apply (impI L). apply eqTrans with (substT t v a). + apply subWithEqualsTerm. apply (sysWeaken L). now apply eqSym. + apply eqTrans with (substT t0 v a). * apply (Axm L); right; constructor. * apply subWithEqualsTerm. now apply (sysWeaken L). - apply (iffE1 L). repeat rewrite subFormulaRelation. apply equalRelation. now apply subWithEqualsTerms. - repeat rewrite subFormulaImp. repeat apply (impI L). apply impE with (substF f1 v a). + apply H0. now repeat apply (sysWeaken L). + apply impE with (substF f0 v a). * apply (Axm L); left; right; constructor. * apply impE with (substF f0 v b). -- apply H. repeat apply (sysWeaken L). now apply eqSym. -- apply (Axm L); right; constructor. - repeat rewrite subFormulaNot. apply (cp2 L), H; now apply eqSym. - decompose record (subFormulaForall2 L a v v0 a0) /r; intros x H2 H1 H3 H5. rewrite H5; clear H5. decompose record (subFormulaForall2 L a v v0 b) /r; intros x0 H5 H4 H6 H8; rewrite H8; clear H8. destruct (eq_nat_dec v v0) as [e | n]. + apply (impRefl L). + set (nv := v0 :: List.remove eq_nat_dec v (freeVarF a) ++ freeVarT a0 ++ freeVarT b) in *. apply (impTrans L) with (forallH (newVar nv) (substF (substF a v (var (newVar nv))) v0 a0)). * apply sysExtend with (Empty_set (fol.Formula L)). intros g H7; destruct H7. apply (impTrans L) with (forallH (newVar nv) (substF (substF (substF a v (var x)) v0 a0) x (var (newVar nv)))). apply (iffE1 L). apply (rebindForall L). unfold not in |- *. intros H7. elim (newVar1 nv). unfold nv at 2 in |- *. assert (H8: In (newVar nv) (freeVarF (substF (substF a v (var x)) v0 a0))) by (eapply in_remove; apply H7). induction (freeVarSubFormula3 _ _ _ _ _ H8). -- assert (In (newVar nv) (freeVarF (substF a v (var x)))) by (eapply in_remove; apply H9). induction (freeVarSubFormula3 _ _ _ _ _ H10). ++ right. apply in_or_app. auto. ++ elim (in_remove_neq _ _ _ _ _ H7). induction H11 as [H11| H11]. auto. contradiction. -- right. auto with datatypes. -- apply (iffE1 L). apply (reduceForall L). apply (notInFreeVarSys L). apply (iffTrans L) with (substF (substF (substF a v (var x)) x (var (newVar nv))) v0 a0). ++ apply (subFormulaExch L); auto. unfold not in |- *; intros. elim (newVar1 nv). unfold nv at 2 in |- *. simpl in |- *. left. induction H7 as [H7| H7]. auto. contradiction. ++ apply (reduceSub L). apply (notInFreeVarSys L). now apply (subFormulaTrans L). * apply (impTrans L) with (forallH (newVar nv) (substF (substF a v (var (newVar nv))) v0 b)). -- apply impE with (equal a0 b). ++ apply sysExtend with (Empty_set (fol.Formula L)). intros f0 H7; destruct H7. repeat apply (impI L). ** apply forallI. unfold not in |- *; intros. destruct H7 as (x1, (H7, H8)). destruct H8 as [x1 H8| x1 H8]; [ induction H8 as [x1 H8| x1 H8] | induction H8 ]. induction H8; simple induction H8. induction H8. simpl in H7. elim (newVar1 nv). unfold nv at 2 in |- *. right. auto with datatypes. elim (in_remove_neq _ _ _ _ _ H7). reflexivity. apply impE with (substF (substF a v (var (newVar nv))) v0 a0). apply H. eapply eqDepth. symmetry in |- *. apply (subFormulaDepth L). apply depthForall. apply (Axm L); left; right; constructor. eapply forallSimp. apply (Axm L); right; constructor. ++ apply H0. -- apply sysExtend with (Empty_set (fol.Formula L)). intros g H7; induction H7. apply (iffE2 L); apply (iffTrans L) with (forallH (newVar nv) (substF (substF (substF a v (var x0)) v0 b) x0 (var (newVar nv)))). apply (rebindForall L). intros H7; elim (newVar1 nv). unfold nv at 2 in |- *. assert (H8: In (newVar nv) (freeVarF (substF (substF a v (var x0)) v0 b))) by (eapply in_remove; apply H7). induction (freeVarSubFormula3 _ _ _ _ _ H8). assert ( H10:In (newVar nv) (freeVarF (substF a v (var x0)))) by (eapply in_remove; apply H9). induction (freeVarSubFormula3 _ _ _ _ _ H10). right; apply in_or_app. now left. elim (in_remove_neq _ _ _ _ _ H7). induction H11 as [H11| H11]. ++ auto. ++ contradiction. ++ right; auto with datatypes. ++ apply (reduceForall L). ** apply (notInFreeVarSys L). ** apply (iffTrans L) with (substF (substF (substF a v (var x0)) x0 (var (newVar nv))) v0 b). apply (subFormulaExch L); auto. intros H7. elim (newVar1 nv). unfold nv at 2 in |- *. simpl in |- *. left. induction H7 as [H7| H7]. auto. contradiction. apply (reduceSub L). apply (notInFreeVarSys L). apply (subFormulaTrans L). auto. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)