Block some annoying reductions that lead to too many unfoldings.

theories/co_pset.v

@@ -151,12 +151,14 @@ Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
 Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
 Definition coPset_all : coPset := coPLeaf true ↾ I.
 Instance coPset_union : Union coPset := λ X Y,
-  (`X ∪ `Y) ↾ coPset_union_wf _ _ (proj2_sig X) (proj2_sig Y).
+  let (t1,Ht1) := X in let (t2,Ht2) := Y in
+  (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
 Instance coPset_intersection : Intersection coPset := λ X Y,
-  (`X ∩ `Y) ↾ coPset_intersection_wf _ _ (proj2_sig X) (proj2_sig Y).
+  let (t1,Ht1) := X in let (t2,Ht2) := Y in
+  (t1 ∩ t2) ↾ coPset_intersection_wf _ _ Ht1 Ht2.
 Instance coPset_difference : Difference coPset := λ X Y,
-  (`X ∩ coPset_opp_raw (`Y)) ↾
-    coPset_intersection_wf _ _ (proj2_sig X) (coPset_opp_wf _).
+  let (t1,Ht1) := X in let (t2,Ht2) := Y in
+  (t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
 
 Instance coPset_elem_of_dec (p : positive) (X : coPset) : Decision (p ∈ X) := _.
 Instance coPset_collection : Collection positive coPset.
@@ -164,11 +166,11 @@ Proof.
   split; [split| |].
   * by intros ??.
   * intros p q. apply elem_of_coPset_singleton.
-  * intros X Y p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
+  * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
     by rewrite elem_of_coPset_union, orb_True.
-  * intros X Y p; unfold elem_of, coPset_elem_of, coPset_intersection; simpl.
+  * intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
     by rewrite elem_of_coPset_intersection, andb_True.
-  * intros X Y p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
+  * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
     by rewrite elem_of_coPset_intersection,
       elem_of_coPset_opp, andb_True, negb_True.
 Qed.
@@ -208,8 +210,10 @@ Lemma coPset_l_wf t : coPset_wf (coPset_l_raw t).
 Proof. induction t as [[]|]; simpl; auto. Qed.
 Lemma coPset_r_wf t : coPset_wf (coPset_r_raw t).
 Proof. induction t as [[]|]; simpl; auto. Qed.
-Definition coPset_l (X : coPset) : coPset := coPset_l_raw (`X) ↾ coPset_l_wf _.
-Definition coPset_r (X : coPset) : coPset := coPset_r_raw (`X) ↾ coPset_r_wf _.
+Definition coPset_l (X : coPset) : coPset :=
+  let (t,Ht) := X in coPset_l_raw t ↾ coPset_l_wf _.
+Definition coPset_r (X : coPset) : coPset :=
+  let (t,Ht) := X in coPset_r_raw t ↾ coPset_r_wf _.
 
 Lemma coPset_lr_disjoint X : coPset_l X ∩ coPset_r X = ∅.
 Proof.
@@ -255,7 +259,7 @@ Proof.
       rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
 Qed.
 Definition to_coPset (X : Pset) : coPset :=
-  to_coPset_raw (pmap_car (mapset_car X)) ↾ to_coPset_raw_wf _ (pmap_prf _).
+  let (m) := X in let (t,Ht) := m in to_coPset_raw t ↾ to_coPset_raw_wf _ Ht.
 Lemma elem_of_to_coPset X i : i ∈ to_coPset X ↔ i ∈ X.
 Proof.
   destruct X as [[t Ht]]; change (e_of i (to_coPset_raw t) ↔ t !! i = Some ()).

theories/pmap.v

@@ -274,15 +274,15 @@ Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)}
 Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
 Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
 Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
-  PMap (partial_alter f i (pmap_car m)) (Ppartial_alter_wf f i _ (pmap_prf m)).
+  let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
 Instance Pfmap : FMap Pmap := λ A B f m,
-  PMap (f <$> pmap_car m) (Pfmap_wf f _ (pmap_prf m)).
+  let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
 Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
-  Pto_list_raw 1 (pmap_car m) [].
+  let (t,Ht) := m in Pto_list_raw 1 t [].
 Instance Pomap : OMap Pmap := λ A B f m,
-  PMap (omap f (pmap_car m)) (Pomap_wf f _ (pmap_prf m)).
+  let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
 Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
-  PMap _ (Pmerge_wf f _ _ (pmap_prf m1) (pmap_prf m2)).
+  let (t1,Ht1) := m1 in let (t2,Ht2) := m2 in PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
 
 Instance Pmap_finmap : FinMap positive Pmap.
 Proof.