-lemma not_epsilon_lp :∀S.∀pi:\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 ((\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 pi) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
-#S #pi (elim pi) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
- [#pi1 #pi2 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * #w1 * #w2 * * #appnil
- cases (\ 5a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"\ 6nil_to_nil\ 5/a\ 6 … appnil) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
- |#p11 #p12 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
- |#pi #H % * #w1 * #w2 * * #appnil (cases (\ 5a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"\ 6nil_to_nil\ 5/a\ 6 … appnil)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+lemma not_epsilon_lp :∀S.∀pi:pitem S. ¬ ((ℓ pi) []).
+#S #pi (elim pi) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace nmk\ 5/span\ 6\ 5/span\ 6/
+ [#pi1 #pi2 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/ * #w1 * #w2 * * #appnil
+ cases (nil_to_nil … appnil) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
+ |#p11 #p12 #H1 #H2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/
+ |#pi #H % * #w1 * #w2 * * #appnil (cases (nil_to_nil … appnil)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace absurd\ 5/span\ 6\ 5/span\ 6/