Theorem: List.conj'_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).conj' = a ⋏ as.conj'
Tactic:
cases as with
| nil => contradiction;
| cons q rs => simp [List.conj']
State after:
no goals

State before:
case nil
F : Type u
inst✝ : LogicalConnective F
p q a : F
h : [] ≠ []
⊢ [a].conj' = a ⋏ [].conj'
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).conj' = a ⋏ (q :: rs).conj'
Tactic:
simp [List.conj']
State after:
no goals