Add Pair_intro

1 files changed, 7 insertions, 0 deletions

diff --git a/Sum.thy b/Sum.thy
index d5704ba..8f40b74 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -57,5 +57,12 @@ lemmas Sum_form_conds [elim] = Sum_form_cond1 Sum_form_cond2
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
   where "A \<times> B \<equiv> \<Sum>_:A. B"
 
+lemma
+  Pair_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : A \<times> B"
+proof
+  fix b B assume "b : B"
+  then show "B : U" ..
+qed
+
 
 end
\ No newline at end of file