Theorem: MM0.lem_4 (FOL/MM0/MM0.lean)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
d : Definition
name : DefName
args : List VarName
h1 : E.WellFormed
h2 : d ∈ E
h3 : name = d.name ∧ args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M E d.F ↔ Holds D I V M E (def_ name args)
Tactic:
induction E
State after:
case nil
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M [] d.F ↔ Holds D I V M [] (def_ name args)

case cons
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  Env.WellFormed tail✝ →
    d ∈ tail✝ →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tail✝ d.F ↔ Holds D I V M tail✝ (def_ name args))
h1 : Env.WellFormed (head✝ :: tail✝)
h2 : d ∈ head✝ :: tail✝
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (head✝ :: tail✝) d.F ↔
    Holds D I V M (head✝ :: tail✝) (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M [] d.F ↔ Holds D I V M [] (def_ name args)
Tactic:
case nil =>
  simp at h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M [] d.F ↔ Holds D I V M [] (def_ name args)
Tactic:
simp at h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
have s1 : Env.Nodup (hd :: tl) := well_formed_env_has_no_dup (hd :: tl) h1
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
have s2 : ∃ E1 : Env, (hd :: tl) = E1 ++ tl
State after:
case s2
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
⊢ ∃ E1, hd :: tl = E1 ++ tl

D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)

State before:
case s2
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
⊢ ∃ E1, hd :: tl = E1 ++ tl

D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
apply Exists.intro [hd]
State after:
case s2
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
⊢ hd :: tl = [hd] ++ tl

D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)

State before:
case s2
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
⊢ hd :: tl = [hd] ++ tl

D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
simp
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
unfold Env.WellFormed at h1
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h2 : d ∈ hd :: tl
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
simp at h2
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
h2 : d = hd ∨ d ∈ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
h2 : d = hd ∨ d ∈ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
left✝ : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
right✝ : IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right : IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
cases h1_right
State after:
case intro
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
left✝ : IsMetaVarOrAllDefInEnv tl hd.F
right✝ : Env.WellFormed tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I V M (hd :: tl) (def_ name args)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    if name = hd.name ∧ args.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F
    else Holds D I V M tl (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    if name = hd.name ∧ args.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F
    else Holds D I V M tl (def_ name args)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
h✝ : name = hd.name ∧ args.length = hd.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F

case neg
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
h✝ : ¬(name = hd.name ∧ args.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
case _ c1 =>
  cases h2
  case inl c2 =>
    subst c2
    simp at c1
    cases h3
    case intro h3_left h3_right =>
      exfalso
      exact c1 h3_left h3_right
  case inr c2 =>
    specialize ih h1_right_right c2
    simp only [← ih]
    apply holds_coincide_env D I (Function.updateListITE V d.args (List.map V args)) M tl (hd :: tl) d.F s2
    apply def_in_well_formed_env_is_meta_var_or_all_def_in_env tl d h1_right_right c2
    exact s1
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : name = hd.name ∧ args.length = hd.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F
Tactic:
cases h2
State after:
case inl
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : name = hd.name ∧ args.length = hd.args.length
h✝ : d = hd
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F

case inr
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : name = hd.name ∧ args.length = hd.args.length
h✝ : d ∈ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : name = hd.name ∧ args.length = hd.args.length
c2 : d = hd
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F
Tactic:
case inl c2 =>
  subst c2
  exact holds_coincide_env D I (Function.updateListITE V d.args (List.map V args)) M tl (d :: tl) d.F s2 h1_right_left s1
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : name = hd.name ∧ args.length = hd.args.length
c2 : d = hd
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F
Tactic:
subst c2
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name ∧ args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔
    Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name ∧ args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔
    Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F
Tactic:
exact holds_coincide_env D I (Function.updateListITE V d.args (List.map V args)) M tl (d :: tl) d.F s2 h1_right_left s1
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : name = hd.name ∧ args.length = hd.args.length
c2 : d ∈ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F
Tactic:
cases h3
State after:
case intro
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : name = hd.name ∧ args.length = hd.args.length
c2 : d ∈ tl
left✝ : name = d.name
right✝ : args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : name = hd.name ∧ args.length = hd.args.length
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F
Tactic:
cases c1
State after:
case intro
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
left✝ : name = hd.name
right✝ : args.length = hd.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V hd.args (List.map V args)) M tl hd.F
Tactic:
exfalso
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ False

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ False
Tactic:
apply h1_left d c2
State after:
case a
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ hd.name = d.name

case a
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ hd.args.length = d.args.length

State before:
case a
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ hd.name = d.name
Tactic:
simp only [← c1_left]
State after:
case a
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ name = d.name

State before:
case a
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ name = d.name
Tactic:
exact h3_left
State after:
no goals

State before:
case a
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ hd.args.length = d.args.length
Tactic:
simp only [← c1_right]
State after:
case a
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ args.length = d.args.length

State before:
case a
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c2 : d ∈ tl
h3_left : name = d.name
h3_right : args.length = d.args.length
c1_left : name = hd.name
c1_right : args.length = hd.args.length
⊢ args.length = d.args.length
Tactic:
exact h3_right
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
cases h2
State after:
case inl
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
h✝ : d = hd
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)

case inr
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
h✝ : d ∈ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d = hd
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
case inl c2 =>
  subst c2
  simp at c1
  cases h3
  case intro h3_left h3_right =>
    exfalso
    exact c1 h3_left h3_right
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
case inr c2 =>
  specialize ih h1_right_right c2
  simp only [← ih]
  apply holds_coincide_env D I (Function.updateListITE V d.args (List.map V args)) M tl (hd :: tl) d.F s2
  apply def_in_well_formed_env_is_meta_var_or_all_def_in_env tl d h1_right_right c2
  exact s1
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d = hd
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
subst c2
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : ¬(name = d.name ∧ args.length = d.args.length)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔ Holds D I V M tl (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : ¬(name = d.name ∧ args.length = d.args.length)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
simp at c1
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name → ¬args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔ Holds D I V M tl (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name → ¬args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
cases h3
State after:
case intro
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name → ¬args.length = d.args.length
left✝ : name = d.name
right✝ : args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔ Holds D I V M tl (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name → ¬args.length = d.args.length
h3_left : name = d.name
h3_right : args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
case intro h3_left h3_right =>
  exfalso
  exact c1 h3_left h3_right
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name → ¬args.length = d.args.length
h3_left : name = d.name
h3_right : args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
exfalso
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name → ¬args.length = d.args.length
h3_left : name = d.name
h3_right : args.length = d.args.length
⊢ False

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name → ¬args.length = d.args.length
h3_left : name = d.name
h3_right : args.length = d.args.length
⊢ False
Tactic:
exact c1 h3_left h3_right
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
specialize ih h1_right_right c2
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
simp only [← ih]
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F
Tactic:
apply holds_coincide_env D I (Function.updateListITE V d.args (List.map V args)) M tl (hd :: tl) d.F s2
State after:
case h2
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ IsMetaVarOrAllDefInEnv tl d.F

case h3
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)

State before:
case h2
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ IsMetaVarOrAllDefInEnv tl d.F

case h3
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)
Tactic:
apply def_in_well_formed_env_is_meta_var_or_all_def_in_env tl d h1_right_right c2
State after:
case h3
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)

State before:
case h3
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)
Tactic:
exact s1
State after:
no goals