Step
*
1
of Lemma
sq_stable__sqle
1. a : Base
2. b : Base
3. ↓a ≤ b
⊢ a ≤ b
BY
{ UseWitness ⌜Ax⌝⋅ }
1
1. a : Base
2. b : Base
3. ↓a ≤ b
⊢ Ax ∈ a ≤ b
Latex:
Latex:
1. a : Base
2. b : Base
3. \mdownarrow{}a \mleq{} b
\mvdash{} a \mleq{} b
By
Latex:
UseWitness \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
Home
Index