∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[0←d]lv] ≗{M} ⟦#i⟧[gv,lv].
#M #HM #gv #lv #d #i
@(mq … HM) [4,5: @(seq_sym … HM) /2 width=2 by ml/ |1,2: skip ]
∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[0←d]lv] ≗{M} ⟦#i⟧[gv,lv].
#M #HM #gv #lv #d #i
@(mq … HM) [4,5: @(seq_sym … HM) /2 width=2 by ml/ |1,2: skip ]