α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 => ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))) s t →
      Computation.LiftRel
        (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
          ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)))
        (destruct s) (destruct t)
α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
⊢ join (append S T) ~ʷ append (join S) (join T)
refine'
  ⟨fun s1 s2 =>
    ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)),
    ⟨nil, S, T, by simp, by simp⟩, _⟩
α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
⊢ Computation.LiftRel
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)))
    (destruct s1) (destruct s2)
α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 => ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))) s t →
      Computation.LiftRel
        (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
          ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)))
        (destruct s) (destruct t)
intro s1 s2 h
α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (fun c1 c2 =>
          ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
        ca cb →
      LiftRelAux
        (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
          ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)))
        (fun c1 c2 =>
          ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
        (Computation.destruct ca) (Computation.destruct cb)
α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
⊢ Computation.LiftRel
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)))
    (destruct s1) (destruct s2)
apply
  lift_rel_rec
    (fun c1 c2 =>
      ∃ (s : WSeq α) (S T : _),
        c1 = destruct (append s (join (append S T))) ∧
          c2 = destruct (append s (append (join S) (join T))))
    _ _ _
    (let ⟨s, S, T, h1, h2⟩ := h
    ⟨s, S, T, congr_arg destruct h1, congr_arg destruct h2⟩)
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
s : WSeq α
S T : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)))
    (fun c1 c2 =>
      ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
    (Computation.destruct (destruct (append s (join (append S T)))))
    (Computation.destruct (destruct (append s (append (join S) (join T)))))
α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (fun c1 c2 =>
          ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
        ca cb →
      LiftRelAux
        (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
          ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)))
        (fun c1 c2 =>
          ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
        (Computation.destruct ca) (Computation.destruct cb)
rintro c1 c2  ⟨s, S, T, rfl, rfl⟩
case intro.intro.intro.intro.h1
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
S T : WSeq (WSeq α)
⊢ LiftRelAux
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) =>
        a = b ∧ ∃ s_1 S T, s = append s_1 (join (append S T)) ∧ t = append s_1 (append (join S) (join T))
      | x, x_2 => False)
    (fun c1 c2 =>
      ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
    (Computation.destruct (destruct (join (append S T)))) (Computation.destruct (destruct (append (join S) (join T))))

case intro.intro.intro.intro.h2
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
S T : WSeq (WSeq α)
a : α
s : WSeq α
⊢ ∃ s_1 S_1 T_1,
    append s (join (append S T)) = append s_1 (join (append S_1 T_1)) ∧
      append s (append (join S) (join T)) = append s_1 (append (join S_1) (join T_1))

case intro.intro.intro.intro.h3
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
S T : WSeq (WSeq α)
s : WSeq α
⊢ ∃ s_1 S_1 T_1,
    destruct (append s (join (append S T))) = destruct (append s_1 (join (append S_1 T_1))) ∧
      destruct (append s (append (join S) (join T))) = destruct (append s_1 (append (join S_1) (join T_1)))
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
s : WSeq α
S T : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)))
    (fun c1 c2 =>
      ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
    (Computation.destruct (destruct (append s (join (append S T)))))
    (Computation.destruct (destruct (append s (append (join S) (join T)))))
induction' s using WSeq.recOn with a s s <;> simp
no goals
α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
⊢ join (append S T) = append nil (join (append S T))
simp
no goals
α : Type u
β : Type v
γ : Type w
S T : WSeq (WSeq α)
⊢ append (join S) (join T) = append nil (append (join S) (join T))
simp
case intro.intro.intro.intro.h1.h1
α : Type u
β : Type v
γ : Type w
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
T : WSeq (WSeq α)
⊢ LiftRelAux
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) =>
        a = b ∧ ∃ s_1 S T, s = append s_1 (join (append S T)) ∧ t = append s_1 (append (join S) (join T))
      | x, x_2 => False)
    (fun c1 c2 =>
      ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
    (Computation.destruct (destruct (join T))) (Computation.destruct (destruct (join T)))

case intro.intro.intro.intro.h1.h2
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
T : WSeq (WSeq α)
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1 T_1,
    destruct (append s (join (append S T))) = destruct (append s_1 (join (append S_1 T_1))) ∧
      destruct (append s (append (join S) (join T))) = destruct (append s_1 (append (join S_1) (join T_1)))

case intro.intro.intro.intro.h1.h3
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
T S : WSeq (WSeq α)
⊢ ∃ s S_1 T_1,
    destruct (join (append S T)) = destruct (append s (join (append S_1 T_1))) ∧
      destruct (append (join S) (join T)) = destruct (append s (append (join S_1) (join T_1)))
case intro.intro.intro.intro.h1
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
S T : WSeq (WSeq α)
⊢ LiftRelAux
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) =>
        a = b ∧ ∃ s_1 S T, s = append s_1 (join (append S T)) ∧ t = append s_1 (append (join S) (join T))
      | x, x_2 => False)
    (fun c1 c2 =>
      ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
    (Computation.destruct (destruct (join (append S T)))) (Computation.destruct (destruct (append (join S) (join T))))
induction' S using WSeq.recOn with s S S <;> simp
case intro.intro.intro.intro.h1.h1.h2
α : Type u
β : Type v
γ : Type w
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
s : WSeq α
T : WSeq (WSeq α)
⊢ ∃ s_1 S T_1,
    destruct (append s (join T)) = destruct (append s_1 (join (append S T_1))) ∧
      destruct (append s (join T)) = destruct (append s_1 (append (join S) (join T_1)))

case intro.intro.intro.intro.h1.h1.h3
α : Type u
β : Type v
γ : Type w
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
T : WSeq (WSeq α)
⊢ ∃ s S T_1,
    destruct (join T) = destruct (append s (join (append S T_1))) ∧
      destruct (join T) = destruct (append s (append (join S) (join T_1)))
case intro.intro.intro.intro.h1.h1
α : Type u
β : Type v
γ : Type w
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
T : WSeq (WSeq α)
⊢ LiftRelAux
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) =>
        a = b ∧ ∃ s_1 S T, s = append s_1 (join (append S T)) ∧ t = append s_1 (append (join S) (join T))
      | x, x_2 => False)
    (fun c1 c2 =>
      ∃ s S T, c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
    (Computation.destruct (destruct (join T))) (Computation.destruct (destruct (join T)))
induction' T using WSeq.recOn with s T T <;> simp
no goals
case intro.intro.intro.intro.h1.h1.h2
α : Type u
β : Type v
γ : Type w
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
s : WSeq α
T : WSeq (WSeq α)
⊢ ∃ s_1 S T_1,
    destruct (append s (join T)) = destruct (append s_1 (join (append S T_1))) ∧
      destruct (append s (join T)) = destruct (append s_1 (append (join S) (join T_1)))
refine' ⟨s, nil, T, _, _⟩ <;> simp
no goals
case intro.intro.intro.intro.h1.h1.h3
α : Type u
β : Type v
γ : Type w
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
T : WSeq (WSeq α)
⊢ ∃ s S T_1,
    destruct (join T) = destruct (append s (join (append S T_1))) ∧
      destruct (join T) = destruct (append s (append (join S) (join T_1)))
refine' ⟨nil, nil, T, _, _⟩ <;> simp
no goals
case intro.intro.intro.intro.h1.h2
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
T : WSeq (WSeq α)
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1 T_1,
    destruct (append s (join (append S T))) = destruct (append s_1 (join (append S_1 T_1))) ∧
      destruct (append s (append (join S) (join T))) = destruct (append s_1 (append (join S_1) (join T_1)))
exact ⟨s, S, T, rfl, rfl⟩
no goals
case intro.intro.intro.intro.h1.h3
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
T S : WSeq (WSeq α)
⊢ ∃ s S_1 T_1,
    destruct (join (append S T)) = destruct (append s (join (append S_1 T_1))) ∧
      destruct (append (join S) (join T)) = destruct (append s (append (join S_1) (join T_1)))
refine' ⟨nil, S, T, _, _⟩ <;> simp
no goals
case intro.intro.intro.intro.h2
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
S T : WSeq (WSeq α)
a : α
s : WSeq α
⊢ ∃ s_1 S_1 T_1,
    append s (join (append S T)) = append s_1 (join (append S_1 T_1)) ∧
      append s (append (join S) (join T)) = append s_1 (append (join S_1) (join T_1))
exact ⟨s, S, T, rfl, rfl⟩
no goals
case intro.intro.intro.intro.h3
α : Type u
β : Type v
γ : Type w
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
S T : WSeq (WSeq α)
s : WSeq α
⊢ ∃ s_1 S_1 T_1,
    destruct (append s (join (append S T))) = destruct (append s_1 (join (append S_1 T_1))) ∧
      destruct (append s (append (join S) (join T))) = destruct (append s_1 (append (join S_1) (join T_1)))
exact ⟨s, S, T, rfl, rfl⟩