α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
⊢ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
cb : Computation β
Hc : C ca cb
a : α
ha : a ∈ ca
⊢ LiftRel R ca cb
revert cb
case refine'_1
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
h : LiftRelAux R C (destruct (pure a)) (destruct cb)
⊢ LiftRel R (pure a) cb

case refine'_2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C (think ca') cb
h : LiftRelAux R C (destruct (think ca')) (destruct cb)
⊢ LiftRel R (think ca') cb
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
⊢ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb
refine' memRecOn (C := (λ ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb))
  ha _ (fun ca' IH => _) <;> intro cb Hc <;> have h := H Hc
case refine'_1
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
h : ∃ b, b ∈ cb ∧ R a b
⊢ LiftRel R (pure a) cb
case refine'_1
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
h : LiftRelAux R C (destruct (pure a)) (destruct cb)
⊢ LiftRel R (pure a) cb
simp at h
no goals
case refine'_1
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
h : ∃ b, b ∈ cb ∧ R a b
⊢ LiftRel R (pure a) cb
simp [h]
case refine'_2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C (think ca') cb
h : LiftRelAux R C (destruct (think ca')) (destruct cb)
⊢ LiftRel R ca' cb
case refine'_2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C (think ca') cb
h : LiftRelAux R C (destruct (think ca')) (destruct cb)
⊢ LiftRel R (think ca') cb
simp
case refine'_2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C (think ca') cb
⊢ LiftRelAux R C (destruct (think ca')) (destruct cb) → LiftRel R ca' cb
case refine'_2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C (think ca') cb
h : LiftRelAux R C (destruct (think ca')) (destruct cb)
⊢ LiftRel R ca' cb
revert h
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C (think ca') cb
cb'✝ : Computation β
h : C ca' cb'✝
⊢ LiftRel R ca' cb'✝
case refine'_2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C (think ca') cb
⊢ LiftRelAux R C (destruct (think ca')) (destruct cb) → LiftRel R ca' cb
apply cb.recOn (fun b => _) fun cb' => _ <;> intros _ h <;> simp at h <;> simp [h]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C (destruct ca) (destruct cb)
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : (fun ca => ∀ (cb : Computation β), C ca cb → LiftRel R ca cb) ca'
cb : Computation β
Hc : C (think ca') cb
cb'✝ : Computation β
h : C ca' cb'✝
⊢ LiftRel R ca' cb'✝
exact IH _ h