Nuprl Rule : universeMemberTYPE
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ T ∈ TYPE
BY universeMemberTYPE !parameter{i:l} ()
H ⊢ T = T ∈ Type
Latex:
H \mvdash{} T \mmember{} TYPE
BY universeMemberTYPE !parameter\{i:l\} ()
H \mvdash{} T = T
Date html generated:
2019_06_20-PM-04_12_17
Last ObjectModification:
2019_03_12-PM-03_13_18
Theory : rules
Home
Index