α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x x_1 => x = x_1) (destruct s) (destruct s)
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x x_1 => x = x_1) (destruct s) (destruct t)
rw [← h]
case H
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Reflexive (LiftRelO R fun x x_1 => x = x_1)
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x x_1 => x = x_1) (destruct s) (destruct s)
apply Computation.LiftRel.refl
case H
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
a : Option (α × WSeq α)
⊢ LiftRelO R (fun x x_1 => x = x_1) a a
case H
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Reflexive (LiftRelO R fun x x_1 => x = x_1)
intro a
case H.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ LiftRelO R (fun x x_1 => x = x_1) none none

case H.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
a : α × WSeq α
⊢ LiftRelO R (fun x x_1 => x = x_1) (some a) (some a)
case H
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
a : Option (α × WSeq α)
⊢ LiftRelO R (fun x x_1 => x = x_1) a a
cases' a with a
no goals
case H.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ LiftRelO R (fun x x_1 => x = x_1) none none
simp
case H.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
fst✝ : α
snd✝ : WSeq α
⊢ LiftRelO R (fun x x_1 => x = x_1) (some (fst✝, snd✝)) (some (fst✝, snd✝))
case H.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
a : α × WSeq α
⊢ LiftRelO R (fun x x_1 => x = x_1) (some a) (some a)
cases a
case H.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
fst✝ : α
snd✝ : WSeq α
⊢ R fst✝ fst✝
case H.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
fst✝ : α
snd✝ : WSeq α
⊢ LiftRelO R (fun x x_1 => x = x_1) (some (fst✝, snd✝)) (some (fst✝, snd✝))
simp only [LiftRelO, and_true]
no goals
case H.some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
fst✝ : α
snd✝ : WSeq α
⊢ R fst✝ fst✝
apply H