Nuprl Lemma : itermMultiply_functionality

[a,b,c,d:int_term()].  (a "*" c ≡ "*" d) supposing (a ≡ and c ≡ d)


Proof




Definitions occuring in Statement :  equiv_int_terms: t1 ≡ t2 itermMultiply: left "*" right int_term: int_term() uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a equiv_int_terms: t1 ≡ t2 all: x:A. B[x] int_term_value: int_term_value(f;t) itermMultiply: left "*" right int_term_ind: int_term_ind prop:
Lemmas referenced :  equiv_int_terms_wf int_term_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution lambdaFormation hypothesis dependent_functionElimination thin hypothesisEquality sqequalRule multiplyEquality functionEquality intEquality lambdaEquality axiomEquality lemma_by_obid isectElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[a,b,c,d:int\_term()].    (a  "*"  c  \mequiv{}  b  "*"  d)  supposing  (a  \mequiv{}  b  and  c  \mequiv{}  d)



Date html generated: 2016_05_14-AM-07_00_01
Last ObjectModification: 2015_12_26-PM-01_12_30

Theory : omega


Home Index