Theorem: List.disj'_cons_nonempty (Logic/Logic/LogicSymbol.lean)

State before:
F : Type u
inst✝ : LogicalConnective F
p q a : F
as : List F
h : as ≠ []
⊢ (a :: as).disj' = a ⋎ as.disj'
Tactic:
cases as with
| nil => contradiction;
| cons q rs => simp [List.disj']
State after:
no goals

State before:
case nil
F : Type u
inst✝ : LogicalConnective F
p q a : F
h : [] ≠ []
⊢ [a].disj' = a ⋎ [].disj'
Tactic:
contradiction
State after:
no goals

State before:
case cons
F : Type u
inst✝ : LogicalConnective F
p q✝ a q : F
rs : List F
h : q :: rs ≠ []
⊢ (a :: q :: rs).disj' = a ⋎ (q :: rs).disj'
Tactic:
simp [List.disj']
State after:
no goals