From b5f98e4da773e402eef152da8ae87d02a772a3bc Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 30 Jun 2018 07:06:19 +0200
Subject: Add Pair_intro

---
 Sum.thy | 7 +++++++
 1 file changed, 7 insertions(+)

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
-- 
cgit v1.2.3