Nuprl Lemma : pscm-ap-comp-term-sq

[Gamma,Delta,Z,s1,s2,t:Top].  ((t)s2 s1 ((t)s2)s1)


Proof




Definitions occuring in Statement :  pscm-ap-term: (t)s pscm-comp: F uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  pscm-comp-term top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalAxiom sqequalRule isect_memberEquality because_Cache

Latex:
\mforall{}[Gamma,Delta,Z,s1,s2,t:Top].    ((t)s2  o  s1  \msim{}  ((t)s2)s1)



Date html generated: 2018_05_22-PM-10_04_40
Last ObjectModification: 2018_05_20-PM-09_49_12

Theory : presheaf!models!of!type!theory


Home Index