internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ (Holds D I V E h1_phi ↔ Holds D I V E h1_psi) ↔ (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi')
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
exact h1_ih_1 V
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_psi h1_psi' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_psi h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I V E h1_psi ↔ Holds D I V E h1_psi'
Tactic:
exact h1_ih_2 V
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_psi)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔ ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_psi
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔ ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_psi
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) E h1_psi
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi ↔ Holds D I (Function.updateITE V h1_x d) E h1_psi
Tactic:
exact h1_ih (Function.updateITE V h1_x d)
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_psi
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi) ↔ ∃ d, Holds D I (Function.updateITE V h1_x d) E h1_psi
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi ↔ Holds D I (Function.updateITE V h1_x a) E h1_psi
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1 : Formula
V : VarAssignment D
⊢ Holds D I V E h1 ↔ Holds D I V E h1
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi' ↔ Holds D I V E h1_phi
Tactic:
symm
Proof state after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' : Formula
a✝ : AlphaEqv h1_phi h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
exact h1_ih V
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi''
Tactic:
trans Holds D I V E h1_phi'
Proof state after:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'

D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
exact h1_ih_1 V
Proof state after:
no goals
Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_phi' h1_phi'' : Formula
a✝¹ : AlphaEqv h1_phi h1_phi'
a✝ : AlphaEqv h1_phi' h1_phi''
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
V : VarAssignment D
⊢ Holds D I V E h1_phi' ↔ Holds D I V E h1_phi''
Tactic:
exact h1_ih_2 V
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarListId
Proof state before:
xs : List VarName
⊢ isAlphaEqvVarList [] xs xs
Tactic:
induction xs
Proof state after:
case nil

⊢ isAlphaEqvVarList [] [] []

case cons
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : isAlphaEqvVarList [] tail✝ tail✝
⊢ isAlphaEqvVarList [] (head✝ :: tail✝) (head✝ :: tail✝)
Theorem: FOL.NV.isAlphaEqvVarListId
Proof state before:
⊢ isAlphaEqvVarList [] [] []
Tactic:
case nil =>
  simp only [isAlphaEqvVarList]
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarListId
Proof state before:
⊢ isAlphaEqvVarList [] [] []
Tactic:
simp only [isAlphaEqvVarList]
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarListId
Proof state before:
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVarList [] (hd :: tl) (hd :: tl)
Tactic:
simp only [isAlphaEqvVarList]
Proof state after:
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd ∧ isAlphaEqvVarList [] tl tl
Theorem: FOL.NV.isAlphaEqvVarListId
Proof state before:
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd ∧ isAlphaEqvVarList [] tl tl
Tactic:
constructor
Proof state after:
case left
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd

case right
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVarList [] tl tl
Theorem: FOL.NV.isAlphaEqvVarListId
Proof state before:
case left
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd
Tactic:
simp only [isAlphaEqvVar]
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarListId
Proof state before:
case right
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVarList [] tl tl
Tactic:
exact ih
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvVar binders x y
⊢ V x = V' y
Tactic:
induction h1
Proof state after:
case nil
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' V✝ : VarAssignment D
h2 : isAlphaEqvVar [] x y
⊢ V✝ x = V✝ y

case cons
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
binders✝ : List (VarName × VarName)
x✝ y✝ : VarName
V✝ V'✝ : VarAssignment D
d✝ : D
a✝ : AlphaEqvVarAssignment D binders✝ V✝ V'✝
a_ih✝ : isAlphaEqvVar binders✝ x y → V✝ x = V'✝ y
h2 : isAlphaEqvVar ((x✝, y✝) :: binders✝) x y
⊢ Function.updateITE V✝ x✝ d✝ x = Function.updateITE V'✝ y✝ d✝ y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : isAlphaEqvVar [] x y
⊢ h1_V x = h1_V y
Tactic:
case nil h1_V =>
  simp only [isAlphaEqvVar] at h2
  subst h2
  rfl
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : isAlphaEqvVar ((h1_x, h1_y) :: h1_l) x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y
Tactic:
case cons h1_l h1_x h1_y h1_V h1_V' h1_d _ h1_ih =>
  simp only [isAlphaEqvVar] at h2
  simp only [Function.updateITE]
  cases h2
  case inl h2 =>
    cases h2
    case intro h2_left h2_right =>
      simp only [if_pos h2_left, if_pos h2_right]
  case inr h2 =>
    cases h2
    case intro h2_left h2_right =>
      cases h2_left
      case intro h2_left_left h2_left_right =>
        simp only [if_neg h2_left_left, if_neg h2_left_right]
        exact h1_ih h2_right
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : isAlphaEqvVar [] x y
⊢ h1_V x = h1_V y
Tactic:
simp only [isAlphaEqvVar] at h2
Proof state after:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : x = y
⊢ h1_V x = h1_V y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : x = y
⊢ h1_V x = h1_V y
Tactic:
subst h2
Proof state after:
D : Type
binders : List (VarName × VarName)
x : VarName
V V' h1_V : VarAssignment D
⊢ h1_V x = h1_V x
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x : VarName
V V' h1_V : VarAssignment D
⊢ h1_V x = h1_V x
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : isAlphaEqvVar ((h1_x, h1_y) :: h1_l) x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y
Tactic:
simp only [isAlphaEqvVar] at h2
Proof state after:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y ∨ (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y ∨ (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y
Tactic:
simp only [Function.updateITE]
Proof state after:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y ∨ (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y ∨ (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
cases h2
Proof state after:
case inl
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h✝ : x = h1_x ∧ y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y

case inr
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h✝ : (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case inl h2 =>
  cases h2
  case intro h2_left h2_right =>
    simp only [if_pos h2_left, if_pos h2_right]
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case inr h2 =>
  cases h2
  case intro h2_left h2_right =>
    cases h2_left
    case intro h2_left_left h2_left_right =>
      simp only [if_neg h2_left_left, if_neg h2_left_right]
      exact h1_ih h2_right
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : x = h1_x ∧ y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
cases h2
Proof state after:
case intro
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
left✝ : x = h1_x
right✝ : y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_left : x = h1_x
h2_right : y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case intro h2_left h2_right =>
  simp only [if_pos h2_left, if_pos h2_right]
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_left : x = h1_x
h2_right : y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
simp only [if_pos h2_left, if_pos h2_right]
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : (¬x = h1_x ∧ ¬y = h1_y) ∧ isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
cases h2
Proof state after:
case intro
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
left✝ : ¬x = h1_x ∧ ¬y = h1_y
right✝ : isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_left : ¬x = h1_x ∧ ¬y = h1_y
h2_right : isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case intro h2_left h2_right =>
  cases h2_left
  case intro h2_left_left h2_left_right =>
    simp only [if_neg h2_left_left, if_neg h2_left_right]
    exact h1_ih h2_right
Proof state after:
no goals
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_left : ¬x = h1_x ∧ ¬y = h1_y
h2_right : isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
cases h2_left
Proof state after:
case intro
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
left✝ : ¬x = h1_x
right✝ : ¬y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
h2_left_left : ¬x = h1_x
h2_left_right : ¬y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
case intro h2_left_left h2_left_right =>
  simp only [if_neg h2_left_left, if_neg h2_left_right]
  exact h1_ih h2_right
Proof state after:
no goals