Nuprl Rule : applyEquality

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

H  ⊢ (f1 a1) = (f2 a2) ∈ B[a1/x]

  BY applyEquality x:A ⟶ B

  H  ⊢ f1 = f2 ∈ (x:A ⟶ B)
  H  ⊢ a1 = a2 ∈ A

Definitions occuring in rule : apply: f a, function: x:A ⟶ B[x], equal: s = t ∈ T, axiom: Ax

Latex:
H \mvdash{} (f1 a1) = (f2 a2) BY applyEquality x:A {}\mrightarrow{} B H \mvdash{} f1 = f2 H \mvdash{} a1 = a2 Date html generated: 2019_06_20-PM-04_11_43 Last ObjectModification: 2016_07_08-PM-03_49_08 Theory : rules Home Index