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

State before:
E : Env
h1 : E.WellFormed
⊢ E.Nodup
Tactic:
induction E
State after:
case nil
h1 : Env.WellFormed []
⊢ Env.Nodup []

case cons
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Env.WellFormed tail✝ → Env.Nodup tail✝
h1 : Env.WellFormed (head✝ :: tail✝)
⊢ Env.Nodup (head✝ :: tail✝)

State before:
h1 : Env.WellFormed []
⊢ Env.Nodup []
Tactic:
case nil =>
  unfold Env.Nodup
  simp
State after:
no goals

State before:
h1 : Env.WellFormed []
⊢ Env.Nodup []
Tactic:
unfold Env.Nodup
State after:
h1 : Env.WellFormed []
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) []

State before:
h1 : Env.WellFormed []
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) []
Tactic:
simp
State after:
no goals

State before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → Env.Nodup tl
h1 : Env.WellFormed (hd :: tl)
⊢ Env.Nodup (hd :: tl)
Tactic:
unfold Env.Nodup at ih
State after:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
h1 : Env.WellFormed (hd :: tl)
⊢ Env.Nodup (hd :: tl)

State before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
h1 : Env.WellFormed (hd :: tl)
⊢ Env.Nodup (hd :: tl)
Tactic:
unfold Env.WellFormed at h1
State after:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Env.Nodup (hd :: tl)

State before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Env.Nodup (hd :: tl)
Tactic:
cases h1
State after:
case intro
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) tl
left✝ : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
right✝ : IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ Env.Nodup (hd :: tl)

State before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ Env.Nodup (hd :: tl)
Tactic:
cases h1_right
State after:
case intro
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ Env.Nodup (hd :: tl)

State before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ Env.Nodup (hd :: tl)
Tactic:
unfold Env.Nodup
State after:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (hd :: tl)

State before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (hd :: tl)
Tactic:
simp
State after:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ (∀ a' ∈ tl, hd.name = a'.name → ¬hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl

State before:
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ (∀ a' ∈ tl, hd.name = a'.name → ¬hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl
Tactic:
constructor
State after:
case left
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ ∀ a' ∈ tl, hd.name = a'.name → ¬hd.args.length = a'.args.length

case right
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl

State before:
case left
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ ∀ a' ∈ tl, hd.name = a'.name → ¬hd.args.length = a'.args.length
Tactic:
exact h1_left
State after:
no goals

State before:
case right
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) 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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl
Tactic:
exact ih h1_right_right
State after:
no goals