simp [inv_def, cancP, eqn]
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
⊢ List.getLast (start :+ (a, b)) nn = (a, !b)⁻¹
no goals