Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_theorem (FOL/NV/Sub/Pred/One/Ind/Sub.lean)

State before:
D : Type
I J : Interpretation D
V : VarAssignment D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h1 : IsSub P zs H A B
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
⊢ Holds D I V E B ↔ Holds D J V E A
Tactic:
induction h1 generalizing V
State after:
case pred_const_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X✝ : PredName
xs✝ : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (pred_const_ X✝ xs✝) ↔ Holds D J V E (pred_const_ X✝ xs✝)

case pred_not_occurs_in
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X✝ : PredName
xs✝ : List VarName
a✝ : ¬(X✝ = P ∧ xs✝.length = zs.length)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (pred_var_ X✝ xs✝) ↔ Holds D J V E (pred_var_ X✝ xs✝)

case pred_occurs_in
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X✝ : PredName
ts✝ : List VarName
a✝¹ : X✝ = P ∧ ts✝.length = zs.length
a✝ : Var.All.Rec.admits (Function.updateListITE id zs ts✝) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs ts✝) H) ↔ Holds D J V E (pred_var_ P ts✝)

case eq_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
x✝ y✝ : VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (eq_ x✝ y✝) ↔ Holds D J V E (eq_ x✝ y✝)

case true_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E true_ ↔ Holds D J V E true_

case false_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E false_ ↔ Holds D J V E false_

case not_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
phi✝ phi'✝ : Formula
a✝ : IsSub P zs H phi✝ phi'✝
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E phi'✝ ↔ Holds D J V E phi✝)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E phi'✝.not_ ↔ Holds D J V E phi✝.not_

case imp_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
phi✝ psi✝ phi'✝ psi'✝ : Formula
a✝¹ : IsSub P zs H phi✝ phi'✝
a✝ : IsSub P zs H psi✝ psi'✝
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E phi'✝ ↔ Holds D J V E phi✝)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E psi'✝ ↔ Holds D J V E psi✝)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (phi'✝.imp_ psi'✝) ↔ Holds D J V E (phi✝.imp_ psi✝)

case and_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
phi✝ psi✝ phi'✝ psi'✝ : Formula
a✝¹ : IsSub P zs H phi✝ phi'✝
a✝ : IsSub P zs H psi✝ psi'✝
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E phi'✝ ↔ Holds D J V E phi✝)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E psi'✝ ↔ Holds D J V E psi✝)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (phi'✝.and_ psi'✝) ↔ Holds D J V E (phi✝.and_ psi✝)

case or_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
phi✝ psi✝ phi'✝ psi'✝ : Formula
a✝¹ : IsSub P zs H phi✝ phi'✝
a✝ : IsSub P zs H psi✝ psi'✝
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E phi'✝ ↔ Holds D J V E phi✝)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E psi'✝ ↔ Holds D J V E psi✝)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (phi'✝.or_ psi'✝) ↔ Holds D J V E (phi✝.or_ psi✝)

case iff_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
phi✝ psi✝ phi'✝ psi'✝ : Formula
a✝¹ : IsSub P zs H phi✝ phi'✝
a✝ : IsSub P zs H psi✝ psi'✝
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E phi'✝ ↔ Holds D J V E phi✝)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E psi'✝ ↔ Holds D J V E psi✝)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (phi'✝.iff_ psi'✝) ↔ Holds D J V E (phi✝.iff_ psi✝)

case forall_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
x✝ : VarName
phi✝ phi'✝ : Formula
a✝¹ : ¬isFreeIn x✝ H
a✝ : IsSub P zs H phi✝ phi'✝
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E phi'✝ ↔ Holds D J V E phi✝)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (forall_ x✝ phi'✝) ↔ Holds D J V E (forall_ x✝ phi✝)

case exists_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
x✝ : VarName
phi✝ phi'✝ : Formula
a✝¹ : ¬isFreeIn x✝ H
a✝ : IsSub P zs H phi✝ phi'✝
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E phi'✝ ↔ Holds D J V E phi✝)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (exists_ x✝ phi'✝) ↔ Holds D J V E (exists_ x✝ phi✝)

case def_
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X✝ : DefName
xs✝ : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (def_ X✝ xs✝) ↔ Holds D J V E (def_ X✝ xs✝)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (pred_const_ h1_X h1_ts) ↔ Holds D J V E (pred_const_ h1_X h1_ts)
Tactic:
case pred_const_ h1_X h1_ts =>
  simp only [Holds]
  simp only [h3_const]
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
case pred_occurs_in h1_X h1_ts h1_1 h1_2 =>
  obtain s1 := Sub.Var.All.Rec.substitution_theorem D I V E (Function.updateListITE id zs h1_ts) H h1_2
  obtain s2 := Function.updateListITE_comp id V zs h1_ts
  simp only [s2] at s1
  simp at s1
  specialize h2 h1_X (List.map V h1_ts)
  simp only [s1] at h2
  simp only [Holds]
  apply h2
  simp
  exact h1_1
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x h1_y : VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (eq_ h1_x h1_y) ↔ Holds D J V E (eq_ h1_x h1_y)
Tactic:
case eq_ h1_x h1_y =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E false_ ↔ Holds D J V E false_
Tactic:
case true_ | false_ =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_phi'.not_ ↔ Holds D J V E h1_phi.not_
Tactic:
case not_ h1_phi h1_phi' _ h1_ih =>
  simp only [Holds]
  congr! 1
  exact h1_ih V h2
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (exists_ h1_x h1_phi') ↔ Holds D J V E (exists_ h1_x h1_phi)
Tactic:
case
  forall_ h1_x h1_phi h1_phi' h1_1 _ h1_ih
| exists_ h1_x h1_phi h1_phi' h1_1 _ h1_ih =>
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply h1_ih
  intro Q ds a1
  specialize h2 Q ds a1
  have s1 :
    Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔
      Holds D I (Function.updateListITE V zs ds) E H :=
    by
    apply Holds_coincide_Var
    intro v a1
    apply Function.updateListITE_updateIte
    intro contra
    subst contra
    contradiction
  simp only [h2] at s1
  exact s1
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (pred_const_ h1_X h1_ts) ↔ Holds D J V E (pred_const_ h1_X h1_ts)
Tactic:
simp only [Holds]
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ I.pred_const_ h1_X (List.map V h1_ts) ↔ J.pred_const_ h1_X (List.map V h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ I.pred_const_ h1_X (List.map V h1_ts) ↔ J.pred_const_ h1_X (List.map V h1_ts)
Tactic:
simp only [h3_const]
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : ¬(h1_X = P ∧ h1_ts.length = zs.length)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (pred_var_ h1_X h1_ts) ↔ Holds D J V E (pred_var_ h1_X h1_ts)
Tactic:
simp at h1_1
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ Holds D I V E (pred_var_ h1_X h1_ts) ↔ Holds D J V E (pred_var_ h1_X h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ Holds D I V E (pred_var_ h1_X h1_ts) ↔ Holds D J V E (pred_var_ h1_X h1_ts)
Tactic:
apply Holds_coincide_PredVar
State after:
case h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ I.pred_const_ = J.pred_const_

case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (pred_var_ h1_X h1_ts) → (I.pred_var_ P ds ↔ J.pred_var_ P ds)

State before:
case h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ I.pred_const_ = J.pred_const_
Tactic:
exact h3_const
State after:
no goals

State before:
case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (pred_var_ h1_X h1_ts) → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
intro X ds a1
State after:
case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
X : PredName
ds : List D
a1 : predVarOccursIn X ds.length (pred_var_ h1_X h1_ts)
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds

State before:
case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
X : PredName
ds : List D
a1 : predVarOccursIn X ds.length (pred_var_ h1_X h1_ts)
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
Tactic:
simp only [predVarOccursIn] at a1
State after:
case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
X : PredName
ds : List D
a1 : X = h1_X ∧ ds.length = h1_ts.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds

State before:
case h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
X : PredName
ds : List D
a1 : X = h1_X ∧ ds.length = h1_ts.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
Tactic:
cases a1
State after:
case h2.intro
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
X : PredName
ds : List D
left✝ : X = h1_X
right✝ : ds.length = h1_ts.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
h1_1 : h1_X = P → ¬h1_ts.length = zs.length
X : PredName
ds : List D
a1_left : X = h1_X
a1_right : ds.length = h1_ts.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
Tactic:
subst a1_left
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ I.pred_var_ X ds ↔ J.pred_var_ X ds
Tactic:
apply h3_var
State after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ ¬(X = P ∧ ds.length = zs.length)

State before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ ¬(X = P ∧ ds.length = zs.length)
Tactic:
simp
State after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ X = P → ¬ds.length = zs.length

State before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
⊢ X = P → ¬ds.length = zs.length
Tactic:
intro a2
State after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
a2 : X = P
⊢ ¬ds.length = zs.length

State before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_ts : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h1_1 : X = P → ¬h1_ts.length = zs.length
a2 : X = P
⊢ ¬ds.length = zs.length
Tactic:
subst a2
State after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : X = X → ¬h1_ts.length = zs.length
⊢ ¬ds.length = zs.length

State before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : X = X → ¬h1_ts.length = zs.length
⊢ ¬ds.length = zs.length
Tactic:
simp at h1_1
State after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
⊢ ¬ds.length = zs.length

State before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
⊢ ¬ds.length = zs.length
Tactic:
intro contra
State after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ False

State before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ False
Tactic:
apply h1_1
State after:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = zs.length

State before:
case a
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = zs.length
Tactic:
trans List.length ds
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = ds.length

D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ ds.length = zs.length

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ h1_ts.length = ds.length
Tactic:
simp only [eq_comm]
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ ds.length = h1_ts.length

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ ds.length = h1_ts.length
Tactic:
exact a1_right
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h1_ts : List VarName
V : VarAssignment D
X : PredName
ds : List D
a1_right : ds.length = h1_ts.length
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = X ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = X ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ X ds)
h1_1 : ¬h1_ts.length = zs.length
contra : ds.length = zs.length
⊢ ds.length = zs.length
Tactic:
exact contra
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
obtain s1 := Sub.Var.All.Rec.substitution_theorem D I V E (Function.updateListITE id zs h1_ts) H h1_2
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
s1 :
  Holds D I (V ∘ Function.updateListITE id zs h1_ts) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
s1 :
  Holds D I (V ∘ Function.updateListITE id zs h1_ts) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
obtain s2 := Function.updateListITE_comp id V zs h1_ts
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
s1 :
  Holds D I (V ∘ Function.updateListITE id zs h1_ts) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
s1 :
  Holds D I (V ∘ Function.updateListITE id zs h1_ts) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
simp only [s2] at s1
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE (V ∘ id) zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE (V ∘ id) zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
simp at s1
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
specialize h2 h1_X (List.map V h1_ts)
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔ J.pred_var_ P (List.map V h1_ts))
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔ J.pred_var_ P (List.map V h1_ts))
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
simp only [s1] at h2
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ Holds D J V E (pred_var_ P h1_ts)
Tactic:
simp only [Holds]
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ J.pred_var_ P (List.map V h1_ts)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔ J.pred_var_ P (List.map V h1_ts)
Tactic:
apply h2
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ h1_X = P ∧ (List.map V h1_ts).length = zs.length

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ h1_X = P ∧ (List.map V h1_ts).length = zs.length
Tactic:
simp
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ h1_X = P ∧ h1_ts.length = zs.length

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_X : PredName
h1_ts : List VarName
h1_1 : h1_X = P ∧ h1_ts.length = zs.length
h1_2 : Var.All.Rec.admits (Function.updateListITE id zs h1_ts) H
V : VarAssignment D
s2 : V ∘ Function.updateListITE id zs h1_ts = Function.updateListITE (V ∘ id) zs (List.map V h1_ts)
s1 :
  Holds D I (Function.updateListITE V zs (List.map V h1_ts)) E H ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H)
h2 :
  h1_X = P ∧ (List.map V h1_ts).length = zs.length →
    (Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs h1_ts) H) ↔
      J.pred_var_ P (List.map V h1_ts))
⊢ h1_X = P ∧ h1_ts.length = zs.length
Tactic:
exact h1_1
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x h1_y : VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (eq_ h1_x h1_y) ↔ Holds D J V E (eq_ h1_x h1_y)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E false_ ↔ Holds D J V E false_
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_phi'.not_ ↔ Holds D J V E h1_phi.not_
Tactic:
simp only [Holds]
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ ¬Holds D I V E h1_phi' ↔ ¬Holds D J V E h1_phi

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ ¬Holds D I V E h1_phi' ↔ ¬Holds D J V E h1_phi
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_phi' ↔ Holds D J V E h1_phi

State before:
case a.h.e'_1.a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_phi' ↔ Holds D J V E h1_phi
Tactic:
exact h1_ih V h2
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
h1_ih_2 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_psi' ↔ Holds D J V E h1_psi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (h1_phi'.iff_ h1_psi') ↔ Holds D J V E (h1_phi.iff_ h1_psi)
Tactic:
simp only [Holds]
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
h1_ih_2 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_psi' ↔ Holds D J V E h1_psi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi') ↔ (Holds D J V E h1_phi ↔ Holds D J V E h1_psi)

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
h1_ih_2 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_psi' ↔ Holds D J V E h1_psi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi') ↔ (Holds D J V E h1_phi ↔ Holds D J V E h1_psi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
h1_ih_2 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_psi' ↔ Holds D J V E h1_psi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_phi' ↔ Holds D J V E h1_phi

case a.h.e'_2.a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
h1_ih_2 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_psi' ↔ Holds D J V E h1_psi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_psi' ↔ Holds D J V E h1_psi

State before:
case a.h.e'_1.a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
h1_ih_2 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_psi' ↔ Holds D J V E h1_psi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_phi' ↔ Holds D J V E h1_phi
Tactic:
exact h1_ih_1 V h2
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_psi h1_phi' h1_psi' : Formula
a✝¹ : IsSub P zs H h1_phi h1_phi'
a✝ : IsSub P zs H h1_psi h1_psi'
h1_ih_1 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
h1_ih_2 :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_psi' ↔ Holds D J V E h1_psi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E h1_psi' ↔ Holds D J V E h1_psi
Tactic:
exact h1_ih_2 V h2
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (exists_ h1_x h1_phi') ↔ Holds D J V E (exists_ h1_x h1_phi)
Tactic:
simp only [Holds]
State after:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi') ↔ ∃ d, Holds D J (Function.updateITE V h1_x d) E h1_phi

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi') ↔ ∃ d, Holds D J (Function.updateITE V h1_x d) E h1_phi
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x a) E h1_phi

State before:
case h
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x a) E h1_phi
Tactic:
intro d
State after:
case h
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x d) E h1_phi

State before:
case h
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
d : D
⊢ Holds D I (Function.updateITE V h1_x d) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply h1_ih
State after:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
d : D
⊢ ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length →
      (Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds)

State before:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
d : D
⊢ ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length →
      (Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds)
Tactic:
intro Q ds a1
State after:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds

State before:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Tactic:
specialize h2 Q ds a1
State after:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds

State before:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Tactic:
have s1 :
  Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔
    Holds D I (Function.updateListITE V zs ds) E H :=
  by
  apply Holds_coincide_Var
  intro v a1
  apply Function.updateListITE_updateIte
  intro contra
  subst contra
  contradiction
State after:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
s1 :
  Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔
    Holds D I (Function.updateListITE V zs ds) E H
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds

State before:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
s1 :
  Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔
    Holds D I (Function.updateListITE V zs ds) E H
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Tactic:
simp only [h2] at s1
State after:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
s1 : Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds

State before:
case h.h2
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
s1 : Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔ J.pred_var_ P ds
Tactic:
exact s1
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ (∀ (d : D), Holds D I (Function.updateITE V h1_x d) E h1_phi') ↔
    ∀ (d : D), Holds D J (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x a) E h1_phi

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ (∃ d, Holds D I (Function.updateITE V h1_x d) E h1_phi') ↔ ∃ d, Holds D J (Function.updateITE V h1_x d) E h1_phi
Tactic:
apply exists_congr
State after:
case h
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ ∀ (a : D), Holds D I (Function.updateITE V h1_x a) E h1_phi' ↔ Holds D J (Function.updateITE V h1_x a) E h1_phi

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ Holds D I (Function.updateListITE (Function.updateITE V h1_x d) zs ds) E H ↔
    Holds D I (Function.updateListITE V zs ds) E H
Tactic:
apply Holds_coincide_Var
State after:
case h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ ∀ (v : VarName),
    isFreeIn v H → Function.updateListITE (Function.updateITE V h1_x d) zs ds v = Function.updateListITE V zs ds v

State before:
case h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1 : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
⊢ ∀ (v : VarName),
    isFreeIn v H → Function.updateListITE (Function.updateITE V h1_x d) zs ds v = Function.updateListITE V zs ds v
Tactic:
intro v a1
State after:
case h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
⊢ Function.updateListITE (Function.updateITE V h1_x d) zs ds v = Function.updateListITE V zs ds v

State before:
case h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
⊢ Function.updateListITE (Function.updateITE V h1_x d) zs ds v = Function.updateListITE V zs ds v
Tactic:
apply Function.updateListITE_updateIte
State after:
case h1.h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
⊢ ¬v = h1_x

State before:
case h1.h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
⊢ ¬v = h1_x
Tactic:
intro contra
State after:
case h1.h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
contra : v = h1_x
⊢ False

State before:
case h1.h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_x : VarName
h1_phi h1_phi' : Formula
h1_1 : ¬isFreeIn h1_x H
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
contra : v = h1_x
⊢ False
Tactic:
subst contra
State after:
case h1.h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
h1_1 : ¬isFreeIn v H
⊢ False

State before:
case h1.h1
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
h1_phi h1_phi' : Formula
a✝ : IsSub P zs H h1_phi h1_phi'
h1_ih :
  ∀ (V : VarAssignment D),
    (∀ (Q : PredName) (ds : List D),
        Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)) →
      (Holds D I V E h1_phi' ↔ Holds D J V E h1_phi)
V : VarAssignment D
d : D
Q : PredName
ds : List D
a1✝ : Q = P ∧ ds.length = zs.length
h2 : Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds
v : VarName
a1 : isFreeIn v H
h1_1 : ¬isFreeIn v H
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I J : Interpretation D
E : Env
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) E H ↔ J.pred_var_ P ds)
⊢ Holds D I V E (def_ X xs) ↔ Holds D J V E (def_ X xs)
Tactic:
cases E
State after:
case nil
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) [] H ↔ J.pred_var_ P ds)
⊢ Holds D I V [] (def_ X xs) ↔ Holds D J V [] (def_ X xs)

case cons
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
head✝ : Definition
tail✝ : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (head✝ :: tail✝) H ↔ J.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (def_ X xs) ↔ Holds D J V (head✝ :: tail✝) (def_ X xs)

State before:
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) [] H ↔ J.pred_var_ P ds)
⊢ Holds D I V [] (def_ X xs) ↔ Holds D J V [] (def_ X xs)
Tactic:
case nil =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) [] H ↔ J.pred_var_ P ds)
⊢ Holds D I V [] (def_ X xs) ↔ Holds D J V [] (def_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
⊢ Holds D I V (hd :: tl) (def_ X xs) ↔ Holds D J V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D J (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D J V tl (def_ X xs)

State before:
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D J (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D J V tl (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D J (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

case neg
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D J V tl (def_ X xs)

State before:
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D J (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
apply Holds_coincide_PredVar
State after:
case h1
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ I.pred_const_ = J.pred_const_

case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length hd.q → (I.pred_var_ P ds ↔ J.pred_var_ P ds)

State before:
case h1
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ I.pred_const_ = J.pred_const_
Tactic:
exact h3_const
State after:
no goals

State before:
case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length hd.q → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet]
State after:
case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), (P, ds.length) ∈ hd.q.predVarSet → (I.pred_var_ P ds ↔ J.pred_var_ P ds)

State before:
case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), (P, ds.length) ∈ hd.q.predVarSet → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp only [hd.h2]
State after:
case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), (P, ds.length) ∈ ∅ → (I.pred_var_ P ds ↔ J.pred_var_ P ds)

State before:
case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), (P, ds.length) ∈ ∅ → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp
State after:
no goals

State before:
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D J V tl (def_ X xs)
Tactic:
apply Holds_coincide_PredVar
State after:
case h1
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ I.pred_const_ = J.pred_const_

case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ X xs) → (I.pred_var_ P ds ↔ J.pred_var_ P ds)

State before:
case h1
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ I.pred_const_ = J.pred_const_
Tactic:
exact h3_const
State after:
no goals

State before:
case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ X xs) → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn]
State after:
case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ J.pred_var_ P ds)

State before:
case h2
D : Type
I J : Interpretation D
A : Formula
P : PredName
zs : List VarName
H B : Formula
h3_const : I.pred_const_ = J.pred_const_
h3_var : ∀ (Q : PredName) (ds : List D), ¬(Q = P ∧ ds.length = zs.length) → (I.pred_var_ Q ds ↔ J.pred_var_ Q ds)
X : DefName
xs : List VarName
V : VarAssignment D
hd : Definition
tl : List Definition
h2 :
  ∀ (Q : PredName) (ds : List D),
    Q = P ∧ ds.length = zs.length → (Holds D I (Function.updateListITE V zs ds) (hd :: tl) H ↔ J.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ J.pred_var_ P ds)
Tactic:
simp
State after:
no goals