case not
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₁✝ ++ L₂✝ <+ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
H : Step L₁ L₂
⊢ L₂ <+ L₁
cases H
case not
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
case not
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₁✝ ++ L₂✝ <+ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
simp
case not.a
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ (x✝, !b✝) :: L₂✝
case not
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
constructor
case not.a.a
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ L₂✝
case not.a
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ (x✝, !b✝) :: L₂✝
constructor
no goals
case not.a.a
α : Type u
L L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₂✝ <+ L₂✝
rfl