-lemma rdeq_inv_zero (h) (o): โY1,Y2. Y1 โ[h, o, #0] Y2 โ
- โจโจ โงโง Y1 = โ & Y2 = โ
- | โโI,L1,L2,V1,V2. L1 โ[h, o, V1] L2 & V1 โ[h, o] V2 &
- Y1 = L1.โ{I}V1 & Y2 = L2.โ{I}V2
- | โโf,I,L1,L2. ๐โฆfโฆ & L1 โชค[cdeq_ext h o, cfull, f] L2 &
- Y1 = L1.โค{I} & Y2 = L2.โค{I}.
-#h #o #Y1 #Y2 #H elim (rex_inv_zero โฆ H) -H *
+lemma rdeq_inv_zero: โY1,Y2. Y1 โ[#0] Y2 โ
+ โจโจ โงโง Y1 = โ & Y2 = โ
+ | โโI,L1,L2,V1,V2. L1 โ[V1] L2 & V1 โ V2 &
+ Y1 = L1.โ{I}V1 & Y2 = L2.โ{I}V2
+ | โโf,I,L1,L2. ๐โฆfโฆ & L1 โชค[cdeq_ext h o, cfull, f] L2 &
+ Y1 = L1.โค{I} & Y2 = L2.โค{I}.
+#Y1 #Y2 #H elim (rex_inv_zero โฆ H) -H *