Theorem: Lean4Lean.VEnv.Ordered.induction (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
case empty
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
⊢ OnTypes ∅ (motive ∅)
Tactic:
exact ⟨nofun, nofun⟩
State after:
no goals

State before:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ (motive env'✝)
Tactic:
apply OnTypes.mono .rfl (mono (addConst_le h3))
State after:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ fun {U} {e A} => motive env✝ U e A

State before:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ fun {U} {e A} => motive env✝ U e A
Tactic:
unfold addConst at h3
State after:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 :
  (match env✝.constants n✝ with
    | some val => none
    | none => some { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }) =
    some env'✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ fun {U} {e A} => motive env✝ U e A

State before:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 :
  (match env✝.constants n✝ with
    | some val => none
    | none => some { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }) =
    some env'✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ fun {U} {e A} => motive env✝ U e A
Tactic:
split at h3 <;> cases h3
State after:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
⊢ OnTypes { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }
    fun {U} {e A} => motive env✝ U e A

State before:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
⊢ OnTypes { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }
    fun {U} {e A} => motive env✝ U e A
Tactic:
refine ⟨fun h => ?_, ih.2⟩
State after:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h :
  { constants := fun n => if n✝¹ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }.constants n✝ =
    some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A

State before:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h :
  { constants := fun n => if n✝¹ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }.constants n✝ =
    some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
simp at h
State after:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h : (if n✝¹ = n✝ then some oci✝ else env✝.constants n✝) = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A

State before:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h : (if n✝¹ = n✝ then some oci✝ else env✝.constants n✝) = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
split at h
State after:
case const.h_2.refl.inl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h : some oci✝ = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A

case const.h_2.refl.inr
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : ¬n✝¹ = n✝
h : env✝.constants n✝ = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A

State before:
case const.h_2.refl.inl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h : some oci✝ = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
cases h
State after:
case const.h_2.refl.inl.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
n✝¹ : Name
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h2 : ∀ (ci : VConstant), some ci✝ = some ci → VConstant.WF env✝ ci
⊢ Exists fun u {U} {e A} => motive env✝ U e A

State before:
case const.h_2.refl.inl.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
n✝¹ : Name
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h2 : ∀ (ci : VConstant), some ci✝ = some ci → VConstant.WF env✝ ci
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
let ⟨_, ht⟩ := h2 _ rfl
State after:
case const.h_2.refl.inl.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
n✝¹ : Name
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h2 : ∀ (ci : VConstant), some ci✝ = some ci → VConstant.WF env✝ ci
w✝ : VLevel
ht : HasType env✝ ci✝.uvars [] ci✝.type (sort w✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A

State before:
case const.h_2.refl.inl.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
n✝¹ : Name
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h2 : ∀ (ci : VConstant), some ci✝ = some ci → VConstant.WF env✝ ci
w✝ : VLevel
ht : HasType env✝ ci✝.uvars [] ci✝.type (sort w✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
exact ⟨_, type h1 ih ht⟩
State after:
no goals

State before:
case const.h_2.refl.inr
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : ¬n✝¹ = n✝
h : env✝.constants n✝ = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
exact ih.1 h
State after:
no goals

State before:
case defeq
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes (addDefEq env✝ df✝) (motive (addDefEq env✝ df✝))
Tactic:
apply OnTypes.mono .rfl (mono addDefEq_le)
State after:
case defeq
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes (addDefEq env✝ df✝) fun {U} {e A} => motive env✝ U e A

State before:
case defeq
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes (addDefEq env✝ df✝) fun {U} {e A} => motive env✝ U e A
Tactic:
refine ⟨ih.1, fun hdf => ?_⟩
State after:
case defeq
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝¹ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝¹
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
hdf : (addDefEq env✝ df✝¹).defeqs df✝
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A

State before:
case defeq
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝¹ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝¹
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
hdf : (addDefEq env✝ df✝¹).defeqs df✝
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A
Tactic:
simp [addDefEq] at hdf
State after:
case defeq
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝¹ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝¹
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
hdf : df✝ = df✝¹ ∨ env✝.defeqs df✝
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A

State before:
case defeq
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝¹ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝¹
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
hdf : df✝ = df✝¹ ∨ env✝.defeqs df✝
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A
Tactic:
obtain rfl | hdf := hdf
State after:
case defeq.inl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
h2 : VDefEq.WF env✝ df✝
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A

case defeq.inr
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝¹ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝¹
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
hdf : env✝.defeqs df✝
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A

State before:
case defeq.inl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
h2 : VDefEq.WF env✝ df✝
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A
Tactic:
let ⟨hl, hr⟩ := h2
State after:
case defeq.inl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
h2 : VDefEq.WF env✝ df✝
hl : HasType env✝ df✝.uvars [] df✝.lhs df✝.type
hr : HasType env✝ df✝.uvars [] df✝.rhs df✝.type
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A

State before:
case defeq.inl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
h2 : VDefEq.WF env✝ df✝
hl : HasType env✝ df✝.uvars [] df✝.lhs df✝.type
hr : HasType env✝ df✝.uvars [] df✝.rhs df✝.type
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A
Tactic:
exact ⟨type h1 ih hl, type h1 ih hr⟩
State after:
no goals

State before:
case defeq.inr
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
df✝¹ : VDefEq
h1 : Ordered env✝
h2 : VDefEq.WF env✝ df✝¹
ih : OnTypes env✝ (motive env✝)
df✝ : VDefEq
hdf : env✝.defeqs df✝
⊢ (fun {U} {e A} => motive env✝ U e A) ∧ fun {U} {e A} => motive env✝ U e A
Tactic:
exact ih.2 hdf
State after:
no goals