Nuprl Lemma : function-eq-symmetry

[A:Type]. ∀[B:Base].
  ∀[f,g:Base].  (function-eq(A;a.B[a];f;g)  function-eq(A;a.B[a];g;f)) supposing base-type-family{i:l}(A;a.B[a])


Proof




Definitions occuring in Statement :  function-eq: function-eq(A;a.B[a];f;g) base-type-family: base-type-family{i:l}(A;a.B[a]) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] implies:  Q base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a implies:  Q function-eq: function-eq(A;a.B[a];f;g) prop: so_lambda: λ2x.t[x] label: ...$L... t so_apply: x[s] subtype_rel: A ⊆B all: x:A. B[x] guard: {T}
Lemmas referenced :  equal-wf-base function-eq_wf base_wf base-type-family_wf base-type-family-implies subtype_rel_self subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution equalitySymmetry hypothesis extract_by_obid isectElimination thin hypothesisEquality sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity cumulativity baseApply closedConclusion baseClosed independent_isectElimination lambdaEquality dependent_functionElimination universeEquality applyEquality hyp_replacement Error :applyLambdaEquality

Latex:
\mforall{}[A:Type].  \mforall{}[B:Base].
    \mforall{}[f,g:Base].    (function-eq(A;a.B[a];f;g)  {}\mRightarrow{}  function-eq(A;a.B[a];g;f)) 
    supposing  base-type-family\{i:l\}(A;a.B[a])



Date html generated: 2016_10_21-AM-09_39_27
Last ObjectModification: 2016_07_12-AM-05_01_25

Theory : per!type


Home Index