α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t u✝ : WSeq α
h1 : LiftRel R s✝ t
h2 : LiftRel R t u✝
s u : WSeq α
h : (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) s u
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (destruct s) (destruct u)
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s t u : WSeq α
h1 : LiftRel R s t
h2 : LiftRel R t u
⊢ LiftRel R s u
refine' ⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => _⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
s u t : WSeq α
h1 : LiftRel R s t
h2 : LiftRel R t u
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (destruct s) (destruct u)
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t u✝ : WSeq α
h1 : LiftRel R s✝ t
h2 : LiftRel R t u✝
s u : WSeq α
h : (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) s u
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (destruct s) (destruct u)
rcases h with ⟨t, h1, h2⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2 : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (destruct s) (destruct u)
case intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
s u t : WSeq α
h1 : LiftRel R s t
h2 : LiftRel R t u
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (destruct s) (destruct u)
have h1 := liftRel_destruct h1
case intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (destruct s) (destruct u)
case intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2 : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (destruct s) (destruct u)
have h2 := liftRel_destruct h2
case intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
a c : Option (α × WSeq α)
ha : a ∈ destruct s
hc : c ∈ destruct u
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
case intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (destruct s) (destruct u)
refine'
  Computation.liftRel_def.2
    ⟨(Computation.terminates_of_LiftRel h1).trans (Computation.terminates_of_LiftRel h2),
      fun {a c} ha hc => _⟩
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
a c : Option (α × WSeq α)
ha : a ∈ destruct s
hc : c ∈ destruct u
b : Option (α × WSeq α)
hb : b ∈ destruct t
t1 : LiftRelO R (LiftRel R) a b
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
case intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
a c : Option (α × WSeq α)
ha : a ∈ destruct s
hc : c ∈ destruct u
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
rcases h1.left ha with ⟨b, hb, t1⟩
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
a c : Option (α × WSeq α)
ha : a ∈ destruct s
hc : c ∈ destruct u
b : Option (α × WSeq α)
hb : b ∈ destruct t
t1 : LiftRelO R (LiftRel R) a b
t2 : LiftRelO R (LiftRel R) b c
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
a c : Option (α × WSeq α)
ha : a ∈ destruct s
hc : c ∈ destruct u
b : Option (α × WSeq α)
hb : b ∈ destruct t
t1 : LiftRelO R (LiftRel R) a b
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
have t2 := Computation.rel_of_LiftRel h2 hb hc
case intro.intro.intro.intro.none.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
ha : none ∈ destruct s
t1 : LiftRelO R (LiftRel R) none b
hc : none ∈ destruct u
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) none none

case intro.intro.intro.intro.none.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
ha : none ∈ destruct s
t1 : LiftRelO R (LiftRel R) none b
c : α × WSeq α
hc : some c ∈ destruct u
t2 : LiftRelO R (LiftRel R) b (some c)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

case intro.intro.intro.intro.some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
a : α × WSeq α
ha : some a ∈ destruct s
t1 : LiftRelO R (LiftRel R) (some a) b
hc : none ∈ destruct u
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) none

case intro.intro.intro.intro.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
a : α × WSeq α
ha : some a ∈ destruct s
t1 : LiftRelO R (LiftRel R) (some a) b
c : α × WSeq α
hc : some c ∈ destruct u
t2 : LiftRelO R (LiftRel R) b (some c)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) (some c)
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
a c : Option (α × WSeq α)
ha : a ∈ destruct s
hc : c ∈ destruct u
b : Option (α × WSeq α)
hb : b ∈ destruct t
t1 : LiftRelO R (LiftRel R) a b
t2 : LiftRelO R (LiftRel R) b c
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
cases' a with a <;> cases' c with c
no goals
case intro.intro.intro.intro.none.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
ha : none ∈ destruct s
t1 : LiftRelO R (LiftRel R) none b
hc : none ∈ destruct u
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) none none
trivial
case intro.intro.intro.intro.none.some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
ha : none ∈ destruct s
c : α × WSeq α
hc : some c ∈ destruct u
hb : none ∈ destruct t
t1 : LiftRelO R (LiftRel R) none none
t2 : LiftRelO R (LiftRel R) none (some c)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

case intro.intro.intro.intro.none.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
ha : none ∈ destruct s
c : α × WSeq α
hc : some c ∈ destruct u
val✝ : α × WSeq α
hb : some val✝ ∈ destruct t
t1 : LiftRelO R (LiftRel R) none (some val✝)
t2 : LiftRelO R (LiftRel R) (some val✝) (some c)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)
case intro.intro.intro.intro.none.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
ha : none ∈ destruct s
t1 : LiftRelO R (LiftRel R) none b
c : α × WSeq α
hc : some c ∈ destruct u
t2 : LiftRelO R (LiftRel R) b (some c)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)
cases b
no goals
case intro.intro.intro.intro.none.some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
ha : none ∈ destruct s
c : α × WSeq α
hc : some c ∈ destruct u
hb : none ∈ destruct t
t1 : LiftRelO R (LiftRel R) none none
t2 : LiftRelO R (LiftRel R) none (some c)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)
cases t2
no goals
case intro.intro.intro.intro.none.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
ha : none ∈ destruct s
c : α × WSeq α
hc : some c ∈ destruct u
val✝ : α × WSeq α
hb : some val✝ ∈ destruct t
t1 : LiftRelO R (LiftRel R) none (some val✝)
t2 : LiftRelO R (LiftRel R) (some val✝) (some c)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)
cases t1
case intro.intro.intro.intro.some.none.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
hc : none ∈ destruct u
t2 : LiftRelO R (LiftRel R) b none
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ destruct s
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) b
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none
case intro.intro.intro.intro.some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
a : α × WSeq α
ha : some a ∈ destruct s
t1 : LiftRelO R (LiftRel R) (some a) b
hc : none ∈ destruct u
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) none
cases a
case intro.intro.intro.intro.some.none.mk.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
hc : none ∈ destruct u
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ destruct s
hb : none ∈ destruct t
t2 : LiftRelO R (LiftRel R) none none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none

case intro.intro.intro.intro.some.none.mk.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
hc : none ∈ destruct u
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ destruct s
b : α × WSeq α
hb : some b ∈ destruct t
t2 : LiftRelO R (LiftRel R) (some b) none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) (some b)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none
case intro.intro.intro.intro.some.none.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
hc : none ∈ destruct u
t2 : LiftRelO R (LiftRel R) b none
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ destruct s
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) b
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none
cases' b with b
no goals
case intro.intro.intro.intro.some.none.mk.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
hc : none ∈ destruct u
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ destruct s
hb : none ∈ destruct t
t2 : LiftRelO R (LiftRel R) none none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none
cases t1
case intro.intro.intro.intro.some.none.mk.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
hc : none ∈ destruct u
fst✝¹ : α
snd✝¹ : WSeq α
ha : some (fst✝¹, snd✝¹) ∈ destruct s
fst✝ : α
snd✝ : WSeq α
hb : some (fst✝, snd✝) ∈ destruct t
t2 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
t1 : LiftRelO R (LiftRel R) (some (fst✝¹, snd✝¹)) (some (fst✝, snd✝))
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝¹, snd✝¹)) none
case intro.intro.intro.intro.some.none.mk.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
hc : none ∈ destruct u
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ destruct s
b : α × WSeq α
hb : some b ∈ destruct t
t2 : LiftRelO R (LiftRel R) (some b) none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) (some b)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none
cases b
no goals
case intro.intro.intro.intro.some.none.mk.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
hc : none ∈ destruct u
fst✝¹ : α
snd✝¹ : WSeq α
ha : some (fst✝¹, snd✝¹) ∈ destruct s
fst✝ : α
snd✝ : WSeq α
hb : some (fst✝, snd✝) ∈ destruct t
t2 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
t1 : LiftRelO R (LiftRel R) (some (fst✝¹, snd✝¹)) (some (fst✝, snd✝))
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝¹, snd✝¹)) none
cases t2
case intro.intro.intro.intro.some.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
c : α × WSeq α
hc : some c ∈ destruct u
t2 : LiftRelO R (LiftRel R) b (some c)
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
t1 : LiftRelO R (LiftRel R) (some (a, s)) b
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
case intro.intro.intro.intro.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
a : α × WSeq α
ha : some a ∈ destruct s
t1 : LiftRelO R (LiftRel R) (some a) b
c : α × WSeq α
hc : some c ∈ destruct u
t2 : LiftRelO R (LiftRel R) b (some c)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) (some c)
cases' a with a s
case intro.intro.intro.intro.some.some.mk.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
c : α × WSeq α
hc : some c ∈ destruct u
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
hb : none ∈ destruct t
t2 : LiftRelO R (LiftRel R) none (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) none
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

case intro.intro.intro.intro.some.some.mk.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
c : α × WSeq α
hc : some c ∈ destruct u
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α × WSeq α
hb : some b ∈ destruct t
t2 : LiftRelO R (LiftRel R) (some b) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
case intro.intro.intro.intro.some.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
b : Option (α × WSeq α)
hb : b ∈ destruct t
c : α × WSeq α
hc : some c ∈ destruct u
t2 : LiftRelO R (LiftRel R) b (some c)
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
t1 : LiftRelO R (LiftRel R) (some (a, s)) b
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
cases' b with b
case intro.intro.intro.intro.some.some.mk.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝
s✝ u t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t✝) (destruct u)
c : α × WSeq α
hc : some c ∈ destruct u
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α
t : WSeq α
hb : some (b, t) ∈ destruct t✝
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
case intro.intro.intro.intro.some.some.mk.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
c : α × WSeq α
hc : some c ∈ destruct u
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α × WSeq α
hb : some b ∈ destruct t
t2 : LiftRelO R (LiftRel R) (some b) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
cases' b with b t
case intro.intro.intro.intro.some.some.mk.some.mk.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t✝) (destruct u✝)
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α
t : WSeq α
hb : some (b, t) ∈ destruct t✝
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
c : α
u : WSeq α
hc : some (c, u) ∈ destruct u✝
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
case intro.intro.intro.intro.some.some.mk.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝
s✝ u t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t✝) (destruct u)
c : α × WSeq α
hc : some c ∈ destruct u
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α
t : WSeq α
hb : some (b, t) ∈ destruct t✝
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
cases' c with c u
case intro.intro.intro.intro.some.some.mk.some.mk.mk.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t✝) (destruct u✝)
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α
t : WSeq α
hb : some (b, t) ∈ destruct t✝
c : α
u : WSeq α
hc : some (c, u) ∈ destruct u✝
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
case intro.intro.intro.intro.some.some.mk.some.mk.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t✝) (destruct u✝)
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α
t : WSeq α
hb : some (b, t) ∈ destruct t✝
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
c : α
u : WSeq α
hc : some (c, u) ∈ destruct u✝
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
cases' t1 with ab st
case intro.intro.intro.intro.some.some.mk.some.mk.mk.intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t✝) (destruct u✝)
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α
t : WSeq α
hb : some (b, t) ∈ destruct t✝
c : α
u : WSeq α
hc : some (c, u) ∈ destruct u✝
ab : R a b
st : LiftRel R s t
bc : R b c
tu : LiftRel R t u
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
case intro.intro.intro.intro.some.some.mk.some.mk.mk.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t✝) (destruct u✝)
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α
t : WSeq α
hb : some (b, t) ∈ destruct t✝
c : α
u : WSeq α
hc : some (c, u) ∈ destruct u✝
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
cases' t2 with bc tu
no goals
case intro.intro.intro.intro.some.some.mk.some.mk.mk.intro.intro
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝¹ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝¹
s✝ u✝ t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u✝
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t✝) (destruct u✝)
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
b : α
t : WSeq α
hb : some (b, t) ∈ destruct t✝
c : α
u : WSeq α
hc : some (c, u) ∈ destruct u✝
ab : R a b
st : LiftRel R s t
bc : R b c
tu : LiftRel R t u
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
exact ⟨H ab bc, t, st, tu⟩
no goals
case intro.intro.intro.intro.some.some.mk.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t)
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct t) (destruct u)
c : α × WSeq α
hc : some c ∈ destruct u
a : α
s : WSeq α
ha : some (a, s) ∈ destruct s✝
hb : none ∈ destruct t
t2 : LiftRelO R (LiftRel R) none (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) none
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
cases t1