Nuprl Lemma : inject-composes

{

[A,B0,B1,C:Type].

[f:A

B0].

[g:B1

C].
    (Inj(A;C;g o f)) supposing
       (Inj(B1;C;g) and
       Inj(A;B0;f) and
       strong-subtype(B0;B1)) }

{ Proof }

Definitions occuring in Statement : inject: Inj(A;B;f), compose: f o g, uimplies: b supposing a, uall:

[x:A]. B[x], function: x:A

B[x], universe: Type, strong-subtype: strong-subtype(A;B)
Definitions : uall:

[x:A]. B[x], uimplies: b supposing a, inject: Inj(A;B;f), member: t

T, all:

x:A. B[x], implies: P

Q, subtype: S

T, suptype: suptype(S; T), compose: f o g, prop:

, strong-subtype: strong-subtype(A;B), cand: A c

B, guard: {T}
Lemmas : compose_wf, inject_wf, strong-subtype_wf

\mforall{}[A,B0,B1,C:Type]. \mforall{}[f:A {}\mrightarrow{} B0]. \mforall{}[g:B1 {}\mrightarrow{} C]. (Inj(A;C;g o f)) supposing (Inj(B1;C;g) and Inj(A;B0;f) and strong-subtype(B0;B1)) Date html generated: 2011_08_16-AM-11_09_50 Last ObjectModification: 2011_06_18-AM-09_42_06 Home Index