α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ Computation.LiftRel
    (LiftRelO R fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t))
    (destruct s) (destruct t)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
⊢ Computation.LiftRel
    (LiftRelO R fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t))
    (destruct s) (destruct t)
have h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t) := by
  cases' h with h h
  exact liftRel_destruct h
  assumption
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ Computation.LiftRel
    (LiftRelO R fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t))
    (destruct s) (destruct t)
apply Computation.LiftRel.imp _ _ _ h
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) a b
intro a b
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) a b
apply LiftRelO.imp_right
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝¹ : WSeq α
t✝¹ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝¹) (destruct t✝¹)
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s✝ t✝
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
intro s t
no goals
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝¹ : WSeq α
t✝¹ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝¹) (destruct t✝¹)
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s✝ t✝
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
apply Or.inl
case inl
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)

case inr
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h : (fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)) s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
cases' h with h h
case inr
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
case inl
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)

case inr
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
exact liftRel_destruct h
no goals
case inr
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝ : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s✝) (destruct t✝)
s : WSeq α
t : WSeq β
h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
assumption