Nuprl Rule : pertypeMemberEquality
This rule proved as lemma rule_pertype_member_equality_true in file rules/rules_pertype.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ t1 = t2 ∈ pertype(R)
BY pertypeMemberEquality !parameter{i:l}
H ⊢ pertype(R) ∈ Type
H ⊢ R t1 t2
H ⊢ t1 ∈ Base
Definitions occuring in rule :
equal: s = t ∈ T,
universe: Type,
pertype: pertype(R),
apply: f a,
member: t ∈ T,
base: Base,
axiom: Ax
Latex:
H \mvdash{} t1 = t2
BY pertypeMemberEquality !parameter\{i:l\}
H \mvdash{} pertype(R) \mmember{} Type
H \mvdash{} R t1 t2
H \mvdash{} t1 \mmember{} Base
Date html generated:
2019_06_20-PM-04_12_10
Last ObjectModification:
2018_09_07-PM-04_30_11
Theory : rules
Home
Index