Theorem: KVChain.rklex.rec (Algdata/Data/KVChain/Basic.lean)

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
⊢ ∀ (h : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays) h
Tactic:
intro h
State after:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
h : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays) h

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
h : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays) h
Tactic:
dsimp [KVChain.rklex, InvImage] at h
State after:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
h : List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList)
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays) h

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
h : List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList)
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays) h
Tactic:
cases h
State after:
case head
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
a✝ : Sigma.lex (flip r) s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))

case tail
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
haxs : boundLeft a₂ xs
a✝ : List.lex (Sigma.lex (flip r) s) xs.toList ys.toList
⊢ motive (KVChain.cons a₂ b₂ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₂ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
hhead : Sigma.lex (flip r) s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
case head hhead =>
  cases hhead
  case fst hheadFst => exact headFst _ _ _ _ _ _ _ _ hheadFst
  case snd hheadSnd => exact headSnd _ _ _ _ _ _ _ hheadSnd
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
haxs : boundLeft a₂ xs
htail : List.lex (Sigma.lex (flip r) s) xs.toList ys.toList
⊢ motive (KVChain.cons a₂ b₂ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₂ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
case tail htail =>
  have := h_ind_ys xs htail
  exact tail _ _ _ _ _ _ htail this
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
hhead : Sigma.lex (flip r) s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
cases hhead
State after:
case fst
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
a✝ : flip r a₁ a₂
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))

case snd
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
b₁ : β a₂
haxs : boundLeft a₂ xs
a✝ : s a₂ b₁ b₂
⊢ motive (KVChain.cons a₂ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
hheadFst : flip r a₁ a₂
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
case fst hheadFst => exact headFst _ _ _ _ _ _ _ _ hheadFst
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
b₁ : β a₂
haxs : boundLeft a₂ xs
hheadSnd : s a₂ b₁ b₂
⊢ motive (KVChain.cons a₂ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
case snd hheadSnd => exact headSnd _ _ _ _ _ _ _ hheadSnd
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
hheadFst : flip r a₁ a₂
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
exact headFst _ _ _ _ _ _ _ _ hheadFst
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
b₁ : β a₂
haxs : boundLeft a₂ xs
hheadSnd : s a₂ b₁ b₂
⊢ motive (KVChain.cons a₂ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
exact headSnd _ _ _ _ _ _ _ hheadSnd
State after:
no goals

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
haxs : boundLeft a₂ xs
htail : List.lex (Sigma.lex (flip r) s) xs.toList ys.toList
⊢ motive (KVChain.cons a₂ b₂ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₂ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
have := h_ind_ys xs htail
State after:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
haxs : boundLeft a₂ xs
htail : List.lex (Sigma.lex (flip r) s) xs.toList ys.toList
this : motive xs ys htail
⊢ motive (KVChain.cons a₂ b₂ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₂ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))

State before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
haxs : boundLeft a₂ xs
htail : List.lex (Sigma.lex (flip r) s) xs.toList ys.toList
this : motive xs ys htail
⊢ motive (KVChain.cons a₂ b₂ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₂ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
exact tail _ _ _ _ _ _ htail this
State after:
no goals