no goals
e : Expr
⊢ Expr.toList e ≠ []
induction e with
| var => simp [Expr.toList]
| op l r ih₁ _   =>
  simp [Expr.toList]
  cases h : l.toList with
  | nil => contradiction
  | cons => simp [List.append]
no goals
case var
x✝ : Nat
⊢ Expr.toList (Expr.var x✝) ≠ []
simp [Expr.toList]
case op
l r : Expr
ih₁ : Expr.toList l ≠ []
rhs_ih✝ : Expr.toList r ≠ []
⊢ ¬Expr.toList l ++ Expr.toList r = []
case op
l r : Expr
ih₁ : Expr.toList l ≠ []
rhs_ih✝ : Expr.toList r ≠ []
⊢ Expr.toList (Expr.op l r) ≠ []
simp [Expr.toList]
no goals
case op
l r : Expr
ih₁ : Expr.toList l ≠ []
rhs_ih✝ : Expr.toList r ≠ []
⊢ ¬Expr.toList l ++ Expr.toList r = []
cases h : l.toList with
| nil => contradiction
| cons => simp [List.append]
no goals
case op.nil
l r : Expr
ih₁ : Expr.toList l ≠ []
rhs_ih✝ : Expr.toList r ≠ []
h : Expr.toList l = []
⊢ ¬[] ++ Expr.toList r = []
contradiction
no goals
case op.cons
l r : Expr
ih₁ : Expr.toList l ≠ []
rhs_ih✝ : Expr.toList r ≠ []
head✝ : Nat
tail✝ : List Nat
h : Expr.toList l = head✝ :: tail✝
⊢ ¬head✝ :: tail✝ ++ Expr.toList r = []
simp [List.append]