Nuprl Rule : pertypeElimination
This rule proved as lemma rule_pertype_elimination2_true in file rules/rules_pertype.v
at https://github.com/vrahli/NuprlInCoq
H x:(t1 = t2 ∈ pertype(R)), J ⊢ C ext e
BY pertypeElimination #$n y ()
H x:(t1 = t2 ∈ pertype(R)), [y:R t1 t2], J ⊢ C ext e
H x:(t1 = t2 ∈ pertype(R)), J ⊢ istype(R t1 t2)
Definitions occuring in rule :
equal: s = t ∈ T,
pertype: pertype(R),
istype: istype(T),
apply: f a,
axiom: Ax
Latex:
H x:(t1 = t2), J \mvdash{} C ext e
BY pertypeElimination \#\$n y ()
H x:(t1 = t2), [y:R t1 t2], J \mvdash{} C ext e
H x:(t1 = t2), J \mvdash{} istype(R t1 t2)
Date html generated:
2019_06_20-PM-04_11_59
Last ObjectModification:
2018_10_04-PM-10_13_28
Theory : rules
Home
Index