Nuprl Rule : hypothesisEquality

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

H x:T, J ⊢ x = x ∈ T

  BY hypothesisEquality #$i

  No Subgoals

Definitions occuring in rule : equal: s = t ∈ T, axiom: Ax

Latex:
H x:T, J \mvdash{} x = x BY hypothesisEquality \#\$i No Subgoals Date html generated: 2019_06_20-PM-04_11_42 Last ObjectModification: 2016_07_08-PM-03_48_57 Theory : rules Home Index