case not
α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
x : α
y : Bool
⊢ Step (FreeGroup.invRev (a ++ (x, y) :: (x, !y) :: b)) (FreeGroup.invRev (a ++ b))
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₁ L₂ : List (α × Bool)
h : Step L₁ L₂
⊢ Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
cases' h with a b x y
no goals
case not
α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
x : α
y : Bool
⊢ Step (FreeGroup.invRev (a ++ (x, y) :: (x, !y) :: b)) (FreeGroup.invRev (a ++ b))
simp [FreeGroup.invRev]