mah...

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 798f5762933b3fd9c1d2153761e08d33e31dc689..14f7aaaa7b982b5d6eb49d4c912fe948bd7572fb 100644 (file)
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -9,8 +9,8 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
-include "basics/types.ma".
-include "arithmetics/nat.ma".
+include "basics/bool.ma".
+(* include "arithmetics/nat.ma". *)
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -31,12 +31,12 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-definition not_nil: ∀A:Type[0].list A → Prop ≝
- λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
+definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
+ λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
 
 theorem nil_cons:
-  ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
-  #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+  ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+  #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/list/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) >Heq //
 qed.
 
 (*
@@ -45,24 +45,24 @@ let rec id_list A (l: list A) on l :=
   [ nil => []
   | (cons hd tl) => hd :: id_list A tl ]. *)
 
-let rec append A (l1: list A) l2 on l1 ≝ 
+let rec append A (l1: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
-  | cons hd tl ⇒  hd :: append A tl l2 ].
+  | cons hd tl ⇒  hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: append A tl l2 ].
 
-definition hd ≝ λA.λl: list A.λd:A.
+definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
   match l with [ nil ⇒ d | cons a _ ⇒ a].
 
-definition tail ≝  λA.λl: list A.
-  match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+definition tail ≝  λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+  match l with [ nil ⇒  \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons hd tl ⇒  tl].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-theorem append_nil: ∀A.∀l:list A.l @ [] = l.
+theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
 #A #l (elim l) normalize // qed.
 
 theorem associative_append: 
- ∀A.associative (list A) (append A).
+ ∀A.\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
 (* deleterio per auto 
@@ -71,50 +71,51 @@ ntheorem cons_append_commute:
     a :: (l1 @ l2) = (a :: l1) @ l2.
 //; nqed. *)
 
-theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
+theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a])\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.
 /2/ qed.
 
-theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
-  l1@l2=[] → P (nil A) (nil A) → P l1 l2.
+theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop. 
+  l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
-theorem nil_to_nil:  ∀A.∀l1,l2:list A.
-  l1@l2 = [] → l1 = [] ∧ l2 = [].
-#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
+theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+  l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+#A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/list/nil_append_elim.def(3)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /2/
 qed.
 
 (* iterators *)
 
-let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
- match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
+ match l with [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: (map A B f tl)].
   
-let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
  
 definition filter ≝ 
-  λT.λp:T → bool.
-  foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
+  λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+  \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p x) (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l0) l0) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
 
-lemma filter_true : ∀A,l,a,p. p a = true → 
-  filter A p (a::l) = a :: filter A p l.
+lemma filter_true : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
+  \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-lemma filter_false : ∀A,l,a,p. p a = false → 
-  filter A p (a::l) = filter A p l.
+lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → 
+  \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
+(*
 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
 match l1 with
-  [ nil ⇒ nil ?
+  [ nil ⇒ nil ?  
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
-  ].
+  ]. *)
 
-(**************************** length ******************************)
+(**************************** length ******************************
 
 let rec length (A:Type[0]) (l:list A) on l ≝ 
   match l with 
@@ -129,12 +130,12 @@ let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝
     [O ⇒ hd A l d
     |S m ⇒ nth m A (tail A l) d].
 
-(**************************** fold *******************************)
+**************************** fold *******************************)
 
-let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
  match l with 
   [ nil ⇒ b 
-  | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
+  | cons a l ⇒ \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p a) (op (f a) (fold A B op b p f l))
       (fold A B op b p f l)].
       
 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
@@ -148,38 +149,38 @@ for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 
 theorem fold_true: 
-∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
-  \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
-    op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
+  \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+    op (f a) \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i). 
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
 theorem fold_false: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
-p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
-  \fold[op,nil]_{i ∈ l| p i} (f i).
+p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+  \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
 theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
-  \fold[op,nil]_{i ∈ l| p i} (f i) = 
-    \fold[op,nil]_{i ∈ (filter A p l)} (f i).
+  \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+    \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l)} (f i).
 #A #B #a #l #p #op #nil #f elim l //  
-#a #tl #Hind cases(true_or_false (p a)) #pa 
-  [ >filter_true // > fold_true // >fold_true //
-  | >filter_false // >fold_false // ]
+#a #tl #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #pa 
+  [ >\ 5a href="cic:/matita/basics/list/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 // > \ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 //
+  | >\ 5a href="cic:/matita/basics/list/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_false.def(3)"\ 6fold_false\ 5/a\ 6 // ]
 qed.
 
 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
   {op :2> A → A → A; 
-   nill:∀a. op nil a = a; 
-   nilr:∀a. op a nil = a;
-   assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+   nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a; 
+   nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
+   assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
   }.
 
-theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
-  op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
-    \fold[op,nil]_{i∈(I@J)} (f i).
+theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/basics/list/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
+  op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈I} (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈J} (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+    \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)} (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
-  [>nill //|#a #tl #Hind <assoc //]
+  [>\ 5a href="cic:/matita/basics/list/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/basics/list/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
 qed.
 

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index c14cc60b4bf4f32ef21f34965932982f2fafdc44..494177cfc11058555764c44e6a9a619e3fe0e27d 100644 (file)
--- a/weblib/basics/types.ma
+++ b/weblib/basics/types.ma
@@ -25,10 +25,10 @@ interpretation "Pair construction" 'pair x y = (pair ? ? x y).
 
 interpretation "Product" 'product x y = (Prod x y).
 
-definition fst ≝ λA,B.λp:A × B.
+definition fst ≝ λA,B.λp:A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
   match p with [pair a b ⇒ a]. 
 
-definition snd ≝ λA,B.λp:A × B.
+definition snd ≝ λA,B.λp:A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
   match p with [pair a b ⇒ b].
 
 interpretation "pair pi1" 'pi1 = (fst ? ?).
@@ -38,8 +38,8 @@ interpretation "pair pi2" 'pi2a x = (snd ? ? x).
 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
 
-theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
-  p = 〈 \fst p, \snd p 〉.
+theorem eq_pair_fst_snd: ∀A,B.∀p:A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B.
+  p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p, \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p 〉.
 #A #B #p (cases p) // qed.
 
 (* sum *)