case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv ((fun o => Option.recOn o nil Prod.snd) <$> destruct s)
    ((fun o => Option.recOn o nil Prod.snd) <$> destruct t)
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ tail s ~ʷ tail t
apply flatten_congr
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv (Computation.bind (destruct s) (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))
    (Computation.bind (destruct t) (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv (Computation.map (fun o => Option.rec nil Prod.snd o) (destruct s))
    (Computation.map (fun o => Option.rec nil Prod.snd o) (destruct t))
rw [← Computation.bind_pure, ← Computation.bind_pure]
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ ∀ {a b : Option (α × WSeq α)},
    BisimO (fun x x_1 => x ~ʷ x_1) a b →
      Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a)
        ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv (Computation.bind (destruct s) (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))
    (Computation.bind (destruct t) (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))
apply liftRel_bind _ _ (destruct_congr h)
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x x_1 => x ~ʷ x_1) a b
⊢ Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a)
    ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
⊢ ∀ {a b : Option (α × WSeq α)},
    BisimO (fun x x_1 => x ~ʷ x_1) a b →
      Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a)
        ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)
intro a b h
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x x_1 => x ~ʷ x_1) a b
⊢ Option.rec nil Prod.snd a ~ʷ Option.rec nil Prod.snd b
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x x_1 => x ~ʷ x_1) a b
⊢ Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a)
    ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)
simp [-liftRel_pure_left, -liftRel_pure_right]
case a.none.none
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
h : BisimO (fun x x_1 => x ~ʷ x_1) none none
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd none

case a.none.some
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) none (some b)
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd (some b)

case a.some.none
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a : α × WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some a) none
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd none

case a.some.some
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)
case a
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x x_1 => x ~ʷ x_1) a b
⊢ Option.rec nil Prod.snd a ~ʷ Option.rec nil Prod.snd b
cases' a with a <;> cases' b with b
no goals
case a.none.none
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
h : BisimO (fun x x_1 => x ~ʷ x_1) none none
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd none
trivial
no goals
case a.none.some
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) none (some b)
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd (some b)
cases h
case a.some.none.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
fst✝ : α
snd✝ : WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some (fst✝, snd✝)) none
⊢ Option.rec nil Prod.snd (some (fst✝, snd✝)) ~ʷ Option.rec nil Prod.snd none
case a.some.none
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a : α × WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some a) none
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd none
cases a
no goals
case a.some.none.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
fst✝ : α
snd✝ : WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some (fst✝, snd✝)) none
⊢ Option.rec nil Prod.snd (some (fst✝, snd✝)) ~ʷ Option.rec nil Prod.snd none
cases h
case a.some.some.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
a : α
s' : WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some b)
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some b)
case a.some.some
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)
cases' a with a s'
case a.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a : α
s' : WSeq α
b : α
t' : WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some (b, t'))
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some (b, t'))
case a.some.some.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
a : α
s' : WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some b)
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some b)
cases' b with b t'
no goals
case a.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h✝ : s ~ʷ t
a : α
s' : WSeq α
b : α
t' : WSeq α
h : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some (b, t'))
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some (b, t'))
exact h.right