12 lines
288 B
Text
12 lines
288 B
Text
Set: pp::colors
|
|
Set: pp::unicode
|
|
Assumed: f
|
|
Assumed: g
|
|
Assumed: a
|
|
Assumed: fid
|
|
Assumed: gcnst
|
|
Proved: one_neq_0
|
|
a
|
|
fid a
|
|
(eqt_elim (trans (trans (congr1 0 (congr2 neq (gcnst a))) neq_to_not_eq)
|
|
(trans (congr2 not (neq_elim one_neq_0)) not_false)))
|