equal
deleted
inserted
replaced
116 sndB "b:Q ==> snd(<a,b>) = b : Q" |
116 sndB "b:Q ==> snd(<a,b>) = b : Q" |
117 pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" |
117 pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" |
118 |
118 |
119 whenBinl "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" |
119 whenBinl "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" |
120 whenBinr "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" |
120 whenBinr "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" |
121 plusEC "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = p : P|Q" |
121 plusEC "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q" |
122 |
122 |
123 applyB "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q" |
123 applyB "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q" |
124 funEC "f:P ==> f = lam x. f`x : P" |
124 funEC "f:P ==> f = lam x. f`x : P" |
125 |
125 |
126 specB "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)" |
126 specB "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)" |