Theorem: KVChain.rklex.rec
Proof 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
Proof 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