+(* Also extracts an equality proof (useful when not using Russell). *)
+notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
+ λ${ident E}.$s ] (refl ? $t) }.
+
+(* Prop sigma *)
+\ 5img class="anchor" src="icons/tick.png" id="PSig"\ 6record PSig (A:Type[0]) (P:A→Prop) : Type[0] ≝
+ {elem:>A; eproof: P elem}.
+
+interpretation "subset type" 'sigma x = (PSig ? x).
+
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+ with precedence 10
+for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒
+ λ${ident E}:$e.$s ] ($refl $T $t) }.
+
+notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
+ match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
+ λ${ident E}.$s ] ] (refl ? $t) }.
+
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+ with precedence 10
+for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒
+ match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
+ λ${ident E}:$J.$s ] ] ($refl $A $t) }.
+
+notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ mk_Prod ${ident w} ${ident x} ⇒ match ${fresh yz} with [ mk_Prod ${ident y} ${ident z} ⇒ $s ] ] ] }.
+
+notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] ] }.
+
+(* This appears to upset automation (previously provable results require greater
+ depth or just don't work), so use example rather than lemma to prevent it
+ being indexed. *)
+\ 5img class="anchor" src="icons/tick.png" id="contract_pair"\ 6example contract_pair : ∀A,B.∀e:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B. (let 〈a,b〉 ≝ e in \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6a,b\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e.
+#A #B * // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="extract_pair"\ 6lemma extract_pair : ∀A,B,C,D. ∀u:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B. ∀Q:A → B → C\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6D. ∀x,y.
+((let 〈a,b〉 ≝ u in Q a b) \ 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\ 6x,y\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6) →
+\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6a,b\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6a,b\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 u \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 Q a b \ 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\ 6x,y\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
+#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 @E1 qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="breakup_pair"\ 6lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
+ R (P (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 x) (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 x)) → R (let 〈a,b〉 ≝ x in P a b).
+#A #B #C *; normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="pair_elim"\ 6lemma pair_elim:
+ ∀A,B,C: Type[0].
+ ∀T: A → B → C.
+ ∀p.
+ ∀P: A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B → C → Prop.
+ (∀lft, rgt. 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\ 6lft,rgt\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 → P \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 (T lft rgt)) →
+ P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
+ #A #B #C #T * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="pair_elim2"\ 6lemma pair_elim2:
+ ∀A,B,C,C': Type[0].
+ ∀T: A → B → C.
+ ∀T': A → B → C'.
+ ∀p.
+ ∀P: A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B → C → C' → Prop.
+ (∀lft, rgt. 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\ 6lft,rgt\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 → P \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 (T lft rgt) (T' lft rgt)) →
+ P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
+ #A #B #C #C' #T #T' * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
\ No newline at end of file