Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux P zs H binders phi
h1_right : admitsAux P zs H binders psi
⊢ (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D (I' D I V' E_ref P zs H) V E_ref psi) ↔
    (Holds D I V E_ref (replace P zs H phi) ↔ Holds D I V E_ref (replace P zs H psi))
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux P zs H binders phi
h1_right : admitsAux P zs H binders psi
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi)

case a.h.e'_2.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux P zs H binders phi
h1_right : admitsAux P zs H binders psi
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi)