equal
deleted
inserted
replaced
124 |
124 |
125 |
125 |
126 subsubsection{*Projections: qfst, qsnd*} |
126 subsubsection{*Projections: qfst, qsnd*} |
127 |
127 |
128 lemma qfst_conv [simp]: "qfst(<a;b>) = a" |
128 lemma qfst_conv [simp]: "qfst(<a;b>) = a" |
129 by (simp add: qfst_def, blast) |
129 by (simp add: qfst_def) |
130 |
130 |
131 lemma qsnd_conv [simp]: "qsnd(<a;b>) = b" |
131 lemma qsnd_conv [simp]: "qsnd(<a;b>) = b" |
132 by (simp add: qsnd_def, blast) |
132 by (simp add: qsnd_def) |
133 |
133 |
134 lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A" |
134 lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A" |
135 by auto |
135 by auto |
136 |
136 |
137 lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))" |
137 lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))" |