α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
      | x, x_2 => False)
    (do
      let x ← destruct (drop s n)
      match x with
        | none => Computation.pure none
        | some (fst, s) => destruct s)
    do
    let x ← destruct (drop t n)
    match x with
      | none => Computation.pure none
      | some (fst, s) => destruct s
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct (drop s (n + 1))) (destruct (drop t (n + 1)))
simp only [LiftRelO, drop, Nat.add_eq, add_zero, destruct_tail, tail.aux]
case h1
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel ?R (destruct (drop s n)) (destruct (drop t n))

case h2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    ?R a b →
      Computation.LiftRel
        (fun x x_1 =>
          match x, x_1 with
          | none, none => True
          | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
          | x, x_2 => False)
        (match a with
        | none => Computation.pure none
        | some (fst, s) => destruct s)
        (match b with
        | none => Computation.pure none
        | some (fst, s) => destruct s)

case R
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Option (α × WSeq α) → Option (β × WSeq β) → Prop
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
      | x, x_2 => False)
    (do
      let x ← destruct (drop s n)
      match x with
        | none => Computation.pure none
        | some (fst, s) => destruct s)
    do
    let x ← destruct (drop t n)
    match x with
      | none => Computation.pure none
      | some (fst, s) => destruct s
apply liftRel_bind
case h2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      Computation.LiftRel
        (fun x x_1 =>
          match x, x_1 with
          | none, none => True
          | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
          | x, x_2 => False)
        (match a with
        | none => Computation.pure none
        | some (fst, s) => destruct s)
        (match b with
        | none => Computation.pure none
        | some (fst, s) => destruct s)
case h1
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel ?R (destruct (drop s n)) (destruct (drop t n))

case h2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    ?R a b →
      Computation.LiftRel
        (fun x x_1 =>
          match x, x_1 with
          | none, none => True
          | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
          | x, x_2 => False)
        (match a with
        | none => Computation.pure none
        | some (fst, s) => destruct s)
        (match b with
        | none => Computation.pure none
        | some (fst, s) => destruct s)

case R
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Option (α × WSeq α) → Option (β × WSeq β) → Prop
apply liftRel_dropn_destruct H n
no goals
case h2
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      Computation.LiftRel
        (fun x x_1 =>
          match x, x_1 with
          | none, none => True
          | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
          | x, x_2 => False)
        (match a with
        | none => Computation.pure none
        | some (fst, s) => destruct s)
        (match b with
        | none => Computation.pure none
        | some (fst, s) => destruct s)
exact fun {a b} o =>
  match a, b, o with
  | none, none, _ => by
    simp [-liftRel_pure_left, -liftRel_pure_right]
  | some (a, s), some (b, t), ⟨_, h2⟩ => by simp [tail.aux]; apply liftRel_destruct h2
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
a : Option (α × WSeq α)
b : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a b
x✝ : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
      | x, x_2 => False)
    (match none with
    | none => Computation.pure none
    | some (fst, s) => destruct s)
    (match none with
    | none => Computation.pure none
    | some (fst, s) => destruct s)
simp [-liftRel_pure_left, -liftRel_pure_right]
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
H : LiftRel R s✝ t✝
n : ℕ
a✝ : Option (α × WSeq α)
b✝ : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a✝ b✝
a : α
s : WSeq α
b : β
t : WSeq β
left✝ : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
      | x, x_2 => False)
    (destruct s) (destruct t)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
H : LiftRel R s✝ t✝
n : ℕ
a✝ : Option (α × WSeq α)
b✝ : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a✝ b✝
a : α
s : WSeq α
b : β
t : WSeq β
left✝ : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
      | x, x_2 => False)
    (match some (a, s) with
    | none => Computation.pure none
    | some (fst, s) => destruct s)
    (match some (b, t) with
    | none => Computation.pure none
    | some (fst, s) => destruct s)
simp [tail.aux]
no goals
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
H : LiftRel R s✝ t✝
n : ℕ
a✝ : Option (α × WSeq α)
b✝ : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a✝ b✝
a : α
s : WSeq α
b : β
t : WSeq β
left✝ : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel
    (fun x x_1 =>
      match x, x_1 with
      | none, none => True
      | some (a, s), some (b, t) => R a b ∧ LiftRel R s t
      | x, x_2 => False)
    (destruct s) (destruct t)
apply liftRel_destruct h2