+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 k}:$X.$eq $T $k $t → $U with [ mk_Prod (${ident xy}:$V) (${ident z}:$Z) ⇒
+ match $xy return λ${ident a}. $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. *)
+example contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
+#A #B * // qed.
+
+lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
+((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
+∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
+#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
+
+lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
+ R (P (\fst x) (\snd x)) → R (let 〈a,b〉 ≝ x in P a b).
+#A #B #C *; normalize /2/
+qed.
+
+lemma pair_elim:
+ ∀A,B,C: Type[0].
+ ∀T: A → B → C.
+ ∀p.
+ ∀P: A×B → C → Prop.
+ (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
+ P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
+ #A #B #C #T * /2/
+qed.
+
+lemma pair_elim2:
+ ∀A,B,C,C': Type[0].
+ ∀T: A → B → C.
+ ∀T': A → B → C'.
+ ∀p.
+ ∀P: A×B → C → C' → Prop.
+ (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (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' * /2/
+qed.
+
+(* Useful for avoiding destruct's full normalization. *)
+lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
+#A #B #a1 #a2 #b1 #b2 #H destruct //
+qed.
+
+lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
+#A #B #a1 #a2 #b1 #b2 #H destruct //
+qed.
+
+lemma pair_destruct_1:
+ ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
+ #A #B #a #b *; /2/
+qed.
+
+lemma pair_destruct_2:
+ ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
+ #A #B #a #b *; /2/
+qed.
+
+lemma coerc_pair_sigma:
+ ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
+#A #B #P * #a #b #p % [@a | /2/]
+qed.
+coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
+≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).