Some cleaning in list representation

FiniteSets/kuratowski/length.v

@@ -11,15 +11,17 @@ Section length.
       apply (if a ∈_d X then n else (S n)).
     - intros X a n.
       simpl.
-      simplify_isIn_d.
-      destruct (dec (a ∈ X)) ; reflexivity.
+      rewrite ?union_isIn_d, singleton_isIn_d_aa.
+      reflexivity.
     - intros X a b n.
       simpl.
-      simplify_isIn_d.
+      rewrite ?union_isIn_d.
       destruct (m_dec_path a b) as [Hab | Hab].
       + strip_truncations.
-        rewrite Hab. simplify_isIn_d. reflexivity.
-      + rewrite ?singleton_isIn_d_false; auto.
+        rewrite Hab.
+        rewrite ?singleton_isIn_d_aa.
+        reflexivity.
+      + rewrite ?singleton_isIn_d_false.
         ++ simpl. 
            destruct (a ∈_d X), (b ∈_d X) ; reflexivity.
         ++ intro p. contradiction (Hab (tr p^)).

FiniteSets/kuratowski/operations.v

@@ -219,18 +219,12 @@ Section FSet_cons_rec.
            (Pcomm : forall X a b p, Pcons a ({|b|} ∪ X) (Pcons b X p)
                                            = Pcons b ({|a|} ∪ X) (Pcons a X p)).
   
-  Definition FSet_cons_rec (X : FSet A) : P.
-  Proof.
-    simple refine (FSetC_ind A (fun _ => P) _ Pe _ _ _ (FSet_to_FSetC X)) ; simpl.
-    - intros a Y p.
-      apply (Pcons a (FSetC_to_FSet Y) p).
-    - intros.
-      refine (transport_const _ _ @ _).
-      apply Pdupl.
-    - intros.
-      refine (transport_const _ _ @ _).
-      apply Pcomm.
-  Defined.
+  Definition FSet_cons_rec (X : FSet A) : P :=
+    FSetC_prim_rec A P Pset Pe
+                   (fun a Y p => Pcons a (FSetC_to_FSet Y) p)
+                   (fun _ _ => Pdupl _ _)
+                   (fun _ _ _ => Pcomm _ _ _)
+                   (FSet_to_FSetC X).
 
   Definition FSet_cons_beta_empty : FSet_cons_rec ∅ = Pe := idpath.
   

FiniteSets/list_representation/list_representation.v

@@ -79,6 +79,27 @@ Module Export FSetC.
       indTy := _; recTy := _;
       H_inductor := FSetC_ind A; H_recursor := FSetC_rec A
     }.
+
+  Section FSetC_prim_recursion.
+    Variable (A : Type)
+             (P : Type)
+             (H : IsHSet P)
+             (nil : P)
+             (cns :  A -> FSetC A -> P -> P)
+             (duplP : forall (a : A) (X : FSetC A) (x : P),
+                 cns a (a ;; X) (cns a X x) = (cns a X x))
+             (commP : forall (a b: A) (X : FSetC A) (x: P),
+                 cns a (b ;; X) (cns b X x) = cns b (a ;; X) (cns a X x)).
+
+    (* Recursion principle *)
+    Definition FSetC_prim_rec : FSetC A -> P.
+    Proof.
+      simple refine (FSetC_ind A (fun _ => P) (fun _ => H) nil cns _ _ );
+        try (intros; simple refine ((transport_const _ _) @ _ ));  cbn.
+      - apply duplP.
+      - apply commP.
+    Defined.
+  End FSetC_prim_recursion.
 End FSetC.
 
 Infix ";;" := Cns (at level 8, right associativity).