topeq Show Code edit
## Equivalence for numerator
thm (topeq () () (-> (z.= A B) (z.= (top A) (top B)))
A B z.headeq
(-> (z.= A B) (z.= (z.head A) (z.head B)))
A df-top z.eqcomi ZeqReplaceImp1Zeq0
(-> (z.= A B) (z.= (top A) (z.head B)))
B df-top z.eqcomi ZeqReplaceImp1Zeq1
(-> (z.= A B) (z.= (top A) (top B)))
)
edit