case H
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = append nil s ∧ s2 = s) (destruct (append nil s)) (destruct s)
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ append nil s = s
apply coinduction2
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append nil s ∧ s2 = s) (destruct (append nil s)) (destruct s)
case H
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = append nil s ∧ s2 = s) (destruct (append nil s)) (destruct s)
intro s
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ match
    destruct
      (corec
        (fun x =>
          match destruct x.fst with
          | none =>
            match destruct x.snd with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.snd))
        (nil, s)),
    destruct s with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append nil s ∧ s2 = s) (destruct (append nil s)) (destruct s)
dsimp [append]
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ match
    omap
      (corec fun x =>
        match destruct x.fst with
        | none =>
          match destruct x.snd with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.snd))
      (match destruct (nil, s).fst with
      | none =>
        match destruct (nil, s).snd with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', (nil, s).snd)),
    destruct s with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ match
    destruct
      (corec
        (fun x =>
          match destruct x.fst with
          | none =>
            match destruct x.snd with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.snd))
        (nil, s)),
    destruct s with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
rw [corec_eq]
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ match
    match
      match destruct s with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    destruct s with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ match
    omap
      (corec fun x =>
        match destruct x.fst with
        | none =>
          match destruct x.snd with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.snd))
      (match destruct (nil, s).fst with
      | none =>
        match destruct (nil, s).snd with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', (nil, s).snd)),
    destruct s with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
dsimp [append]
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ match
    match
      match destruct nil with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    destruct nil with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ ∀ (x : α) (s : Seq α),
    match
      match
        match destruct (cons x s) with
        | none => none
        | some (a, b) => some (a, nil, b) with
      | none => none
      | some (a, b) =>
        some
          (a,
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              b),
      destruct (cons x s) with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ s_1,
          s =
              corec
                (fun x =>
                  match destruct x.fst with
                  | none =>
                    match destruct x.snd with
                    | none => none
                    | some (a, b) => some (a, nil, b)
                  | some (a, s₁') => some (a, s₁', x.snd))
                (nil, s_1) ∧
            s' = s_1
    | x, x_1 => False
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ match
    match
      match destruct s with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    destruct s with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
apply recOn s _ _
no goals
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ match
    match
      match destruct nil with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    destruct nil with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
trivial
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ match
    match
      match destruct (cons x s) with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    destruct (cons x s) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ ∀ (x : α) (s : Seq α),
    match
      match
        match destruct (cons x s) with
        | none => none
        | some (a, b) => some (a, nil, b) with
      | none => none
      | some (a, b) =>
        some
          (a,
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              b),
      destruct (cons x s) with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ s_1,
          s =
              corec
                (fun x =>
                  match destruct x.fst with
                  | none =>
                    match destruct x.snd with
                    | none => none
                    | some (a, b) => some (a, nil, b)
                  | some (a, s₁') => some (a, s₁', x.snd))
                (nil, s_1) ∧
            s' = s_1
    | x, x_1 => False
intro x s
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ match
    match
      match some (x, s) with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    some (x, s) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ match
    match
      match destruct (cons x s) with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    destruct (cons x s) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
rw [destruct_cons]
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ x = x ∧
    ∃ s_1,
      corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            (nil, s) =
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            (nil, s_1) ∧
        s = s_1
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ match
    match
      match some (x, s) with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    some (x, s) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match destruct x.fst with
                | none =>
                  match destruct x.snd with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
dsimp
no goals
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ x = x ∧
    ∃ s_1,
      corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            (nil, s) =
          corec
            (fun x =>
              match destruct x.fst with
              | none =>
                match destruct x.snd with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            (nil, s_1) ∧
        s = s_1
exact ⟨rfl, s, rfl, rfl⟩