α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 =>
          ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
        s t →
      Computation.LiftRel
        (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
          ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
        (destruct s) (destruct t)
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
⊢ join (join SS) ~ʷ join (map join SS)
refine'
  ⟨fun s1 s2 =>
    ∃ s S SS,
      s1 = append s (join (append S (join SS))) ∧
        s2 = append s (append (join S) (join (map join SS))),
    ⟨nil, nil, SS, by simp, by simp⟩, _⟩
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
⊢ Computation.LiftRel
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
    (destruct s1) (destruct s2)
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 =>
          ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
        s t →
      Computation.LiftRel
        (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
          ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
        (destruct s) (destruct t)
intro s1 s2 h
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (fun c1 c2 =>
          ∃ s S SS,
            c1 = destruct (append s (join (append S (join SS)))) ∧
              c2 = destruct (append s (append (join S) (join (map join SS)))))
        ca cb →
      LiftRelAux
        (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
          ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
        (fun c1 c2 =>
          ∃ s S SS,
            c1 = destruct (append s (join (append S (join SS)))) ∧
              c2 = destruct (append s (append (join S) (join (map join SS)))))
        (Computation.destruct ca) (Computation.destruct cb)
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
⊢ Computation.LiftRel
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
    (destruct s1) (destruct s2)
apply
  lift_rel_rec
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    _ (destruct s1) (destruct s2)
    (let ⟨s, S, SS, h1, h2⟩ := h
    ⟨s, S, SS, by simp [h1], by simp [h2]⟩)
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h✝ : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
h :
  ∃ s S SS,
    c1 = destruct (append s (join (append S (join SS)))) ∧
      c2 = destruct (append s (append (join S) (join (map join SS))))
⊢ LiftRelAux
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    (Computation.destruct c1) (Computation.destruct c2)
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (fun c1 c2 =>
          ∃ s S SS,
            c1 = destruct (append s (join (append S (join SS)))) ∧
              c2 = destruct (append s (append (join S) (join (map join SS)))))
        ca cb →
      LiftRelAux
        (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
          ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
        (fun c1 c2 =>
          ∃ s S SS,
            c1 = destruct (append s (join (append S (join SS)))) ∧
              c2 = destruct (append s (append (join S) (join (map join SS)))))
        (Computation.destruct ca) (Computation.destruct cb)
intro c1 c2 h
no goals
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
⊢ join (join SS) = append nil (join (append nil (join SS)))
simp
no goals
α : Type u
β : Type v
γ : Type w
SS : WSeq (WSeq (WSeq α))
⊢ join (map join SS) = append nil (append (join nil) (join (map join SS)))
simp
no goals
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
h1 : s1 = append s (join (append S (join SS)))
h2 : s2 = append s (append (join S) (join (map join SS)))
⊢ destruct s1 = destruct (append s (join (append S (join SS))))
simp [h1]
no goals
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
h1 : s1 = append s (join (append S (join SS)))
h2 : s2 = append s (append (join S) (join (map join SS)))
⊢ destruct s2 = destruct (append s (append (join S) (join (map join SS))))
simp [h2]
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    (Computation.destruct (destruct (append s (join (append S (join SS))))))
    (Computation.destruct (destruct (append s (append (join S) (join (map join SS))))))
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h✝ : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
h :
  ∃ s S SS,
    c1 = destruct (append s (join (append S (join SS)))) ∧
      c2 = destruct (append s (append (join S) (join (map join SS))))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    (Computation.destruct (destruct (append s (join (append S (join SS))))))
    (Computation.destruct (destruct (append s (append (join S) (join (map join SS))))))
clear h
case h1
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (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 SS, s = append s_1 (join (append S (join SS))) ∧ t = append s_1 (append (join S) (join (map join SS)))
      | x, x_2 => False)
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    (Computation.destruct (destruct (join (append S (join SS)))))
    (Computation.destruct (destruct (append (join S) (join (map join SS)))))

case h2
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
a : α
s : WSeq α
⊢ ∃ s_1 S_1 SS_1,
    append s (join (append S (join SS))) = append s_1 (join (append S_1 (join SS_1))) ∧
      append s (append (join S) (join (map join SS))) = append s_1 (append (join S_1) (join (map join SS_1)))

case h3
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
s : WSeq α
⊢ ∃ s_1 S_1 SS_1,
    destruct (append s (join (append S (join SS)))) = destruct (append s_1 (join (append S_1 (join SS_1)))) ∧
      destruct (append s (append (join S) (join (map join SS)))) =
        destruct (append s_1 (append (join S_1) (join (map join SS_1))))
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 =>
      ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS))))
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    (Computation.destruct (destruct (append s (join (append S (join SS))))))
    (Computation.destruct (destruct (append s (append (join S) (join (map join SS))))))
induction' s using WSeq.recOn with a s s <;> simp
case h1.h1
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (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 SS, s = append s_1 (join (append S (join SS))) ∧ t = append s_1 (append (join S) (join (map join SS)))
      | x, x_2 => False)
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    (Computation.destruct (destruct (join (join SS)))) (Computation.destruct (destruct (join (map join SS))))

case h1.h2
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1 SS_1,
    destruct (append s (join (append S (join SS)))) = destruct (append s_1 (join (append S_1 (join SS_1)))) ∧
      destruct (append s (append (join S) (join (map join SS)))) =
        destruct (append s_1 (append (join S_1) (join (map join SS_1))))

case h1.h3
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ ∃ s S_1 SS_1,
    destruct (join (append S (join SS))) = destruct (append s (join (append S_1 (join SS_1)))) ∧
      destruct (append (join S) (join (map join SS))) = destruct (append s (append (join S_1) (join (map join SS_1))))
case h1
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (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 SS, s = append s_1 (join (append S (join SS))) ∧ t = append s_1 (append (join S) (join (map join SS)))
      | x, x_2 => False)
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    (Computation.destruct (destruct (join (append S (join SS)))))
    (Computation.destruct (destruct (append (join S) (join (map join SS)))))
induction' S using WSeq.recOn with s S S <;> simp
case h1.h1.h2
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ ∃ s S_1 SS_1,
    destruct (join (append S (join SS))) = destruct (append s (join (append S_1 (join SS_1)))) ∧
      destruct (append (join S) (join (map join SS))) = destruct (append s (append (join S_1) (join (map join SS_1))))

case h1.h1.h3
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ ∃ s S SS_1,
    destruct (join (join SS)) = destruct (append s (join (append S (join SS_1)))) ∧
      destruct (join (map join SS)) = destruct (append s (append (join S) (join (map join SS_1))))
case h1.h1
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (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 SS, s = append s_1 (join (append S (join SS))) ∧ t = append s_1 (append (join S) (join (map join SS)))
      | x, x_2 => False)
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = destruct (append s (join (append S (join SS)))) ∧
          c2 = destruct (append s (append (join S) (join (map join SS)))))
    (Computation.destruct (destruct (join (join SS)))) (Computation.destruct (destruct (join (map join SS))))
induction' SS using WSeq.recOn with S SS SS <;> simp
no goals
case h1.h1.h2
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ ∃ s S_1 SS_1,
    destruct (join (append S (join SS))) = destruct (append s (join (append S_1 (join SS_1)))) ∧
      destruct (append (join S) (join (map join SS))) = destruct (append s (append (join S_1) (join (map join SS_1))))
refine' ⟨nil, S, SS, _, _⟩ <;> simp
no goals
case h1.h1.h3
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ ∃ s S SS_1,
    destruct (join (join SS)) = destruct (append s (join (append S (join SS_1)))) ∧
      destruct (join (map join SS)) = destruct (append s (append (join S) (join (map join SS_1))))
refine' ⟨nil, nil, SS, _, _⟩ <;> simp
no goals
case h1.h2
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1 SS_1,
    destruct (append s (join (append S (join SS)))) = destruct (append s_1 (join (append S_1 (join SS_1)))) ∧
      destruct (append s (append (join S) (join (map join SS)))) =
        destruct (append s_1 (append (join S_1) (join (map join SS_1))))
exact ⟨s, S, SS, rfl, rfl⟩
no goals
case h1.h3
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ ∃ s S_1 SS_1,
    destruct (join (append S (join SS))) = destruct (append s (join (append S_1 (join SS_1)))) ∧
      destruct (append (join S) (join (map join SS))) = destruct (append s (append (join S_1) (join (map join SS_1))))
refine' ⟨nil, S, SS, _, _⟩ <;> simp
no goals
case h2
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
a : α
s : WSeq α
⊢ ∃ s_1 S_1 SS_1,
    append s (join (append S (join SS))) = append s_1 (join (append S_1 (join SS_1))) ∧
      append s (append (join S) (join (map join SS))) = append s_1 (append (join S_1) (join (map join SS_1)))
exact ⟨s, S, SS, rfl, rfl⟩
no goals
case h3
α : Type u
β : Type v
γ : Type w
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = append s (join (append S (join SS))) ∧ s2 = append s (append (join S) (join (map join SS)))
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
s : WSeq α
⊢ ∃ s_1 S_1 SS_1,
    destruct (append s (join (append S (join SS)))) = destruct (append s_1 (join (append S_1 (join SS_1)))) ∧
      destruct (append s (append (join S) (join (map join SS)))) =
        destruct (append s_1 (append (join S_1) (join (map join SS_1))))
exact ⟨s, S, SS, rfl, rfl⟩