∀[Info,E,dom,l,R,locless,pred,rank,info,x:Top]. (loc(x) ~ l x)
BY { Intros }
1 1. [Info] : Top 2. [E] : Top 3. [dom] : Top 4. [l] : Top 5. [R] : Top 6. [locless] : Top 7. [pred] : Top 8. [rank] : Top 9. [info] : Top 10. [x] : Top ⊢ loc(x) ~ l x
Latex:
Latex:
\mforall{}[Info,E,dom,l,R,locless,pred,rank,info,x:Top]. (loc(x) \msim{} l x)