Nuprl Rule : pertypeEquality

This rule proved as lemma rule_pertype_equality_true in file rules/rules_pertype.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ pertype(R) = pertype(R') ∈ Type

  BY pertypeEquality x y z u v ()

  H x:Base, y:Base ⊢ R x y ∈ Type
  H x:Base, y:Base ⊢ R' x y ∈ Type
  H x:Base, y:Base, z:R x y ⊢ R' x y
  H x:Base, y:Base, z:R' x y ⊢ R x y
  H x:Base, y:Base, z:R x y ⊢ R y x
  H x:Base, y:Base, z:Base, u:R x y, v:R y z ⊢ R x z

Definitions occuring in rule : equal: s = t ∈ T, pertype: pertype(R), member: t ∈ T, universe: Type, base: Base, apply: f a, axiom: Ax

Latex:
H \mvdash{} pertype(R) = pertype(R') BY pertypeEquality x y z u v () H x:Base, y:Base \mvdash{} R x y \mmember{} Type H x:Base, y:Base \mvdash{} R' x y \mmember{} Type H x:Base, y:Base, z:R x y \mvdash{} R' x y H x:Base, y:Base, z:R' x y \mvdash{} R x y H x:Base, y:Base, z:R x y \mvdash{} R y x H x:Base, y:Base, z:Base, u:R x y, v:R y z \mvdash{} R x z Date html generated: 2019_06_20-PM-04_12_17 Last ObjectModification: 2016_07_08-PM-03_48_50 Theory : rules Home Index