let s be SynTypes_Calculus; for T, Y being FinSequence of s
for x, y, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds
(T ^ <*(y \ x)*>) ^ Y ==>. z
let T, Y be FinSequence of s; for x, y, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds
(T ^ <*(y \ x)*>) ^ Y ==>. z
let x, y, z be type of s; ( T ==>. y & <*x*> ^ Y ==>. z implies (T ^ <*(y \ x)*>) ^ Y ==>. z )
assume that
A1:
T ==>. y
and
A2:
<*x*> ^ Y ==>. z
; (T ^ <*(y \ x)*>) ^ Y ==>. z
(H2(s) ^ <*x*>) ^ Y ==>. z
by A2, FINSEQ_1:34;
then
((H2(s) ^ T) ^ <*(y \ x)*>) ^ Y ==>. z
by A1, Def18;
hence
(T ^ <*(y \ x)*>) ^ Y ==>. z
by FINSEQ_1:34; verum