α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
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) => S a b ∧ ∃ s_1, s = map f1 s_1 ∧ ∃ x, t = map f2 x ∧ LiftRel R s_1 x
      | x, x_2 => False)
    (Computation.map (Option.map (Prod.map f1 (map f1))) (destruct s))
    (Computation.map (Option.map (Prod.map f2 (map f2))) (destruct t))
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO S fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t)
    (destruct (map f1 s)) (destruct (map f2 t))
simp [destruct_map]
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      match Option.map (Prod.map f1 (map f1)) a, Option.map (Prod.map f2 (map f2)) b with
      | none, none => True
      | some (a, s), some (b, t) => S a b ∧ ∃ s_1, s = map f1 s_1 ∧ ∃ x, t = map f2 x ∧ LiftRel R s_1 x
      | x, x_1 => False
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
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) => S a b ∧ ∃ s_1, s = map f1 s_1 ∧ ∃ x, t = map f2 x ∧ LiftRel R s_1 x
      | x, x_2 => False)
    (Computation.map (Option.map (Prod.map f1 (map f1))) (destruct s))
    (Computation.map (Option.map (Prod.map f2 (map f2))) (destruct t))
apply Computation.liftRel_map _ _ (liftRel_destruct h)
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
⊢ match Option.map (Prod.map f1 (map f1)) o, Option.map (Prod.map f2 (map f2)) p with
  | none, none => True
  | some (a, s), some (b, t) => S a b ∧ ∃ s_1, s = map f1 s_1 ∧ ∃ x, t = map f2 x ∧ LiftRel R s_1 x
  | x, x_1 => False
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      match Option.map (Prod.map f1 (map f1)) a, Option.map (Prod.map f2 (map f2)) b with
      | none, none => True
      | some (a, s), some (b, t) => S a b ∧ ∃ s_1, s = map f1 s_1 ∧ ∃ x, t = map f2 x ∧ LiftRel R s_1 x
      | x, x_1 => False
intro o p h
case none.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
b : β × WSeq β
h : LiftRelO R (LiftRel R) none (some b)
⊢ False

case some.none
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) none
⊢ False

case some.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ S (f1 a.fst) (f2 b.fst) ∧ ∃ s, map f1 a.snd = map f1 s ∧ ∃ x, map f2 b.snd = map f2 x ∧ LiftRel R s x
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
⊢ match Option.map (Prod.map f1 (map f1)) o, Option.map (Prod.map f2 (map f2)) p with
  | none, none => True
  | some (a, s), some (b, t) => S a b ∧ ∃ s_1, s = map f1 s_1 ∧ ∃ x, t = map f2 x ∧ LiftRel R s_1 x
  | x, x_1 => False
cases' o with a <;> cases' p with b <;> simp
case none.some.mk
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
fst✝ : β
snd✝ : WSeq β
h : LiftRelO R (LiftRel R) none (some (fst✝, snd✝))
⊢ False
case none.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
b : β × WSeq β
h : LiftRelO R (LiftRel R) none (some b)
⊢ False
cases b
no goals
case none.some.mk
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
fst✝ : β
snd✝ : WSeq β
h : LiftRelO R (LiftRel R) none (some (fst✝, snd✝))
⊢ False
cases h
case some.none.mk
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
fst✝ : α
snd✝ : WSeq α
h : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
⊢ False
case some.none
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) none
⊢ False
cases a
no goals
case some.none.mk
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
fst✝ : α
snd✝ : WSeq α
h : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
⊢ False
cases h
case some.some.mk
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s✝ : WSeq α
t : WSeq β
h✝ : LiftRel R s✝ t
b : β × WSeq β
a : α
s : WSeq α
h : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ S (f1 (a, s).fst) (f2 b.fst) ∧ ∃ s_1, map f1 (a, s).snd = map f1 s_1 ∧ ∃ x, map f2 b.snd = map f2 x ∧ LiftRel R s_1 x
case some.some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (some a) (some b)
⊢ S (f1 a.fst) (f2 b.fst) ∧ ∃ s, map f1 a.snd = map f1 s ∧ ∃ x, map f2 b.snd = map f2 x ∧ LiftRel R s x
cases' a with a s
case some.some.mk.mk
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s✝ : WSeq α
t✝ : WSeq β
h✝ : LiftRel R s✝ t✝
a : α
s : WSeq α
b : β
t : WSeq β
h : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ S (f1 (a, s).fst) (f2 (b, t).fst) ∧
    ∃ s_1, map f1 (a, s).snd = map f1 s_1 ∧ ∃ x, map f2 (b, t).snd = map f2 x ∧ LiftRel R s_1 x
case some.some.mk
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s✝ : WSeq α
t : WSeq β
h✝ : LiftRel R s✝ t
b : β × WSeq β
a : α
s : WSeq α
h : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ S (f1 (a, s).fst) (f2 b.fst) ∧ ∃ s_1, map f1 (a, s).snd = map f1 s_1 ∧ ∃ x, map f2 b.snd = map f2 x ∧ LiftRel R s_1 x
cases' b with b t
case some.some.mk.mk.intro
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s✝ : WSeq α
t✝ : WSeq β
h✝ : LiftRel R s✝ t✝
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ S (f1 (a, s).fst) (f2 (b, t).fst) ∧
    ∃ s_1, map f1 (a, s).snd = map f1 s_1 ∧ ∃ x, map f2 (b, t).snd = map f2 x ∧ LiftRel R s_1 x
case some.some.mk.mk
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s✝ : WSeq α
t✝ : WSeq β
h✝ : LiftRel R s✝ t✝
a : α
s : WSeq α
b : β
t : WSeq β
h : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ S (f1 (a, s).fst) (f2 (b, t).fst) ∧
    ∃ s_1, map f1 (a, s).snd = map f1 s_1 ∧ ∃ x, map f2 (b, t).snd = map f2 x ∧ LiftRel R s_1 x
cases' h with r h
no goals
case some.some.mk.mk.intro
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s✝ : WSeq α
t✝ : WSeq β
h✝ : LiftRel R s✝ t✝
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ S (f1 (a, s).fst) (f2 (b, t).fst) ∧
    ∃ s_1, map f1 (a, s).snd = map f1 s_1 ∧ ∃ x, map f2 (b, t).snd = map f2 x ∧ LiftRel R s_1 x
exact ⟨h2 r, s, rfl, t, rfl, h⟩