α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel
    (LiftRelO R fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) (destruct s)
    (destruct t)
apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) a b
intro a b
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) a b
apply LiftRelO.imp_right
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝¹ : WSeq α
t✝¹ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝¹ t✝¹
s✝ : WSeq α
t✝ : WSeq β
h : LiftRel R s✝ t✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1
intro s t
no goals
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝¹ : WSeq α
t✝¹ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝¹ t✝¹
s✝ : WSeq α
t✝ : WSeq β
h : LiftRel R s✝ t✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1
apply Or.inl
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h : LiftRel R s1 t1
⊢ 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (Computation.bind (destruct s1) fun x =>
      match x with
      | none => destruct s2
      | some (a, s) => Computation.pure (some (a, append s s2)))
    (Computation.bind (destruct t1) fun x =>
      match x with
      | none => destruct t2
      | some (a, s) => Computation.pure (some (a, append s t2)))
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h : LiftRel R s1 t1
⊢ Computation.LiftRel
    (LiftRelO R fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1)
    (destruct (append s1 s2)) (destruct (append t1 t2))
simp [destruct_append]
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h : LiftRel R s1 t1
⊢ ∀ {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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
          | x, x_2 => False)
        (match a with
        | none => destruct s2
        | some (a, s) => Computation.pure (some (a, append s s2)))
        (match b with
        | none => destruct t2
        | some (a, s) => Computation.pure (some (a, append s t2)))
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h : LiftRel R s1 t1
⊢ 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (Computation.bind (destruct s1) fun x =>
      match x with
      | none => destruct s2
      | some (a, s) => Computation.pure (some (a, append s s2)))
    (Computation.bind (destruct t1) fun x =>
      match x with
      | none => destruct t2
      | some (a, s) => Computation.pure (some (a, append s t2)))
apply Computation.liftRel_bind _ _ (liftRel_destruct h)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
⊢ 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match o with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match p with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h : LiftRel R s1 t1
⊢ ∀ {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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
          | x, x_2 => False)
        (match a with
        | none => destruct s2
        | some (a, s) => Computation.pure (some (a, append s s2)))
        (match b with
        | none => destruct t2
        | some (a, s) => Computation.pure (some (a, append s t2)))
intro o p h
case none.none
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match none with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match none with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))

case none.some
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
b : β × WSeq β
h : LiftRelO R (LiftRel R) none (some 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match none with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some b with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))

case some.none
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some a with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match none with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))

case some.some
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some a with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some b with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
⊢ 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match o with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match p with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
cases' o with a <;> cases' p with b
case none.none
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (destruct s2) (destruct t2)
case none.none
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match none with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match none with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
simp
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      match a, b with
      | none, none => True
      | some (a, s), some (b, t) =>
        R a b ∧ (LiftRel R s t ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_1 => False
case none.none
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (destruct s2) (destruct t2)
apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h2)
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    match a, b with
    | none, none => True
    | some (a, s), some (b, t) =>
      R a b ∧ (LiftRel R s t ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
    | x, x_1 => False
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      match a, b with
      | none, none => True
      | some (a, s), some (b, t) =>
        R a b ∧ (LiftRel R s t ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_1 => False
intro a b
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    match a, b with
    | none, none => True
    | some (a, s), some (b, t) =>
      R a b ∧ (LiftRel R s t ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
    | x, x_1 => False
apply LiftRelO.imp_right
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x
intro s t
no goals
case H
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x
apply Or.inl
case none.some.mk
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
fst✝ : β
snd✝ : WSeq β
h : LiftRelO R (LiftRel R) none (some (fst✝, snd✝))
⊢ 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match none with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some (fst✝, snd✝) with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
case none.some
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
b : β × WSeq β
h : LiftRelO R (LiftRel R) none (some 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match none with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some b with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
cases b
no goals
case none.some.mk
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
fst✝ : β
snd✝ : WSeq β
h : LiftRelO R (LiftRel R) none (some (fst✝, snd✝))
⊢ 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match none with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some (fst✝, snd✝) with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
cases h
case some.none.mk
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
fst✝ : α
snd✝ : WSeq α
h : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some (fst✝, snd✝) with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match none with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
case some.none
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some a with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match none with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
cases a
no goals
case some.none.mk
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
fst✝ : α
snd✝ : WSeq α
h : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some (fst✝, snd✝) with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match none with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
cases h
case some.some.mk
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
b : β × WSeq β
a : α
s : WSeq α
h : LiftRelO R (LiftRel R) (some (a, s)) (some 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some (a, s) with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some b with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
case some.some
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some a with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some b with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
cases' a with a s
case some.some.mk.mk
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
h : LiftRelO R (LiftRel R) (some (a, s)) (some (b, 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some (a, s) with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some (b, t) with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
case some.some.mk
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
b : β × WSeq β
a : α
s : WSeq α
h : LiftRelO R (LiftRel R) (some (a, s)) (some 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some (a, s) with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some b with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
cases' b with b t
case some.some.mk.mk.intro
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some (a, s) with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some (b, t) with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
case some.some.mk.mk
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
h : LiftRelO R (LiftRel R) (some (a, s)) (some (b, 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some (a, s) with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some (b, t) with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
cases' h with r h
case some.some.mk.mk.intro
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ R a b ∧
    (LiftRel R (append s s2) (append t t2) ∨
      ∃ s1, append s s2 = append s1 s2 ∧ ∃ x, append t t2 = append x t2 ∧ LiftRel R s1 x)
case some.some.mk.mk.intro
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : 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 ∨ ∃ s1, s = append s1 s2 ∧ ∃ x, t = append x t2 ∧ LiftRel R s1 x)
      | x, x_2 => False)
    (match some (a, s) with
    | none => destruct s2
    | some (a, s) => Computation.pure (some (a, append s s2)))
    (match some (b, t) with
    | none => destruct t2
    | some (a, s) => Computation.pure (some (a, append s t2)))
simp [-liftRel_pure_left, -liftRel_pure_right]
no goals
case some.some.mk.mk.intro
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ R a b ∧
    (LiftRel R (append s s2) (append t t2) ∨
      ∃ s1, append s s2 = append s1 s2 ∧ ∃ x, append t t2 = append x t2 ∧ LiftRel R s1 x)
exact ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩