Library kuratowski.length
Require Import HoTT HitTactics prelude interfaces.lattice_interface interfaces.lattice_examples.
Require Import kuratowski.operations kuratowski.properties kuratowski.kuratowski_sets isomorphism.
Section length.
Context {A : Type} `{MerelyDecidablePaths A} `{Univalence}.
Definition length : FSet A → nat.
simple refine (FSet_cons_rec _ _ _ _ _ _).
- apply 0.
- intros a X n.
apply (if a ∈_d X then n else (S n)).
- intros X a n.
simpl.
rewrite ?union_isIn_d, singleton_isIn_d_aa.
reflexivity.
- intros X a b n.
simpl.
rewrite ?union_isIn_d.
destruct (m_dec_path a b) as [Hab | Hab].
+ strip_truncations.
rewrite Hab.
reflexivity.
+ rewrite ?singleton_isIn_d_false.
++ simpl.
destruct (a ∈_d X), (b ∈_d X) ; reflexivity.
++ intro p. contradiction (Hab (tr p^)).
++ intros p.
apply (Hab (tr p)).
Defined.
Open Scope nat.
Require Import kuratowski.operations kuratowski.properties kuratowski.kuratowski_sets isomorphism.
Section length.
Context {A : Type} `{MerelyDecidablePaths A} `{Univalence}.
Definition length : FSet A → nat.
simple refine (FSet_cons_rec _ _ _ _ _ _).
- apply 0.
- intros a X n.
apply (if a ∈_d X then n else (S n)).
- intros X a n.
simpl.
rewrite ?union_isIn_d, singleton_isIn_d_aa.
reflexivity.
- intros X a b n.
simpl.
rewrite ?union_isIn_d.
destruct (m_dec_path a b) as [Hab | Hab].
+ strip_truncations.
rewrite Hab.
reflexivity.
+ rewrite ?singleton_isIn_d_false.
++ simpl.
destruct (a ∈_d X), (b ∈_d X) ; reflexivity.
++ intro p. contradiction (Hab (tr p^)).
++ intros p.
apply (Hab (tr p)).
Defined.
Open Scope nat.
Specification for length.
Definition length_empty : length ∅ = 0 := idpath.
Definition length_singleton a : length {|a|} = 1 := idpath.
Lemma length_compute (a : A) (X : FSet A) :
length ({|a|} ∪ X) = if (a ∈_d X) then length X else S(length X).
Proof.
unfold length.
rewrite FSet_cons_beta_cons.
reflexivity.
Defined.
Definition length_add (a : A) (X : FSet A) (p : a ∈_d X = false)
: length ({|a|} ∪ X) = 1 + (length X).
Proof.
rewrite length_compute.
destruct (a ∈_d X).
- contradiction (true_ne_false).
- reflexivity.
Defined.
Definition disjoint X Y := X ∩ Y = ∅.
Lemma disjoint_difference X Y : disjoint X (difference Y X).
Proof.
apply ext.
intros a.
rewrite intersection_isIn_d, empty_isIn_d, difference_isIn_d.
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
Defined.
Lemma disjoint_sub a X Y (H1 : disjoint ({|a|} ∪ X) Y) : disjoint X Y.
Proof.
unfold disjoint in ×.
apply ext.
intros b.
simplify_isIn_d.
rewrite empty_isIn_d.
pose (ap (fun Z ⇒ b ∈_d Z) H1) as p.
simpl in p.
rewrite intersection_isIn_d, empty_isIn_d, union_isIn_d in p.
destruct (b ∈_d X), (b ∈_d Y) ; try reflexivity.
- destruct (b ∈_d {|a|}) ; simpl in × ; try (contradiction true_ne_false).
Defined.
Definition length_disjoint (X Y : FSet A) :
∀ (HXY : disjoint X Y),
length (X ∪ Y) = (length X) + (length Y).
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _ X)
; try (intros ; apply path_ishprop) ; simpl.
- intros.
apply (ap length (nl _)).
- intros a X1 HX1 HX1Y.
rewrite <- assoc, ?length_compute, ?union_isIn_d in ×.
pose (ap (fun Z ⇒ a ∈_d Z) HX1Y) as p.
simpl in p.
rewrite intersection_isIn_d, union_isIn_d, singleton_isIn_d_aa, empty_isIn_d in p.
assert (orb (a ∈_d X1) (a ∈_d Y) = a ∈_d X1) as HaY.
{ destruct (a ∈_d X1), (a ∈_d Y) ; try reflexivity.
contradiction true_ne_false.
}
rewrite ?HaY, HX1.
destruct (a ∈_d X1) ; try reflexivity.
apply (disjoint_sub a X1 Y HX1Y).
Defined.
Lemma set_as_difference X Y : X = (difference X Y) ∪ (X ∩ Y).
Proof.
toBool.
generalize (a ∈_d X), (a ∈_d Y).
intros b c ; destruct b, c ; reflexivity.
Defined.
Lemma length_single_disjoint (X Y : FSet A) :
length X = length (difference X Y) + length (X ∩ Y).
Proof.
refine (ap length (set_as_difference X Y) @ _).
apply length_disjoint.
apply ext.
intros a.
rewrite ?intersection_isIn_d, empty_isIn_d, difference_isIn_d.
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
Defined.
Lemma union_to_disjoint X Y : X ∪ Y = X ∪ (difference Y X).
Proof.
toBool.
generalize (a ∈_d X), (a ∈_d Y).
intros b c ; destruct b, c ; reflexivity.
Defined.
Lemma length_union_1 (X Y : FSet A) :
length (X ∪ Y) = length X + length (difference Y X).
Proof.
refine (ap length (union_to_disjoint X Y) @ _).
apply length_disjoint.
apply ext.
intros a.
rewrite ?intersection_isIn_d, empty_isIn_d, difference_isIn_d.
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
Defined.
Lemma plus_assoc n m k : n + (m + k) = (n + m) + k.
Proof.
induction n ; simpl.
- reflexivity.
- rewrite IHn.
reflexivity.
Defined.
Lemma inclusion_exclusion (X Y : FSet A) :
length (X ∪ Y) + length (Y ∩ X) = length X + length Y.
Proof.
rewrite length_union_1.
rewrite (length_single_disjoint Y X).
rewrite plus_assoc.
reflexivity.
Defined.
End length.
Section length_product.
Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B} `{Univalence}.
Theorem length_singleproduct (a : A) (X : FSet B)
: length (single_product a X) = length X.
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _ X)
; try (intros ; apply path_ishprop) ; simpl.
- reflexivity.
- intros b X1 HX1.
rewrite ?length_compute, ?HX1.
enough(b ∈_d X1 = (a, b) ∈_d (single_product a X1)) as HE.
{ rewrite HE ; reflexivity. }
rewrite singleproduct_isIn_d_aa ; try reflexivity.
Defined.
Open Scope nat.
Lemma single_product_disjoint (a : A) (X1 : FSet A) (Y : FSet B)
: sum (prod (a ∈_d X1 = true)
((single_product a Y) ∪ (product X1 Y) = (product X1 Y)))
(prod (a ∈_d X1 = false)
(disjoint (single_product a Y) (product X1 Y))).
Proof.
pose (b := a ∈_d X1).
assert (a ∈_d X1 = b) as HaX1.
{ reflexivity. }
destruct b.
× refine (inl(HaX1,_)).
apply ext.
intros [a1 b1].
rewrite ?union_isIn_d.
unfold member_dec, fset_member_bool in ×.
destruct (dec ((a1, b1) ∈ (single_product a Y))) as [t | t]
; destruct (dec ((a1, b1) ∈ (product X1 Y))) as [p | p]
; try reflexivity.
rewrite singleproduct_isIn in t.
destruct t as [t1 t2].
rewrite product_isIn in p.
strip_truncations.
rewrite <- t1 in HaX1.
destruct (dec (a1 ∈ X1)) ; try (contradiction false_ne_true).
contradiction (p(t,t2)).
× refine (inr(HaX1,_)).
apply ext.
intros [a1 b1].
rewrite intersection_isIn_d, empty_isIn_d.
unfold member_dec, fset_member_bool in ×.
destruct (dec ((a1, b1) ∈ (single_product a Y))) as [t | t]
; destruct (dec ((a1, b1) ∈ (product X1 Y))) as [p | p]
; try reflexivity.
rewrite singleproduct_isIn in t ; destruct t as [t1 t2].
rewrite product_isIn in p ; destruct p as [p1 p2].
strip_truncations.
rewrite t1 in p1.
destruct (dec (a ∈ X1)).
** contradiction true_ne_false.
** contradiction (n p1).
Defined.
Theorem length_product (X : FSet A) (Y : FSet B)
: length (product X Y) = length X × length Y.
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _ X)
; try (intros ; apply path_ishprop) ; simpl.
- reflexivity.
- intros a X1 HX1.
rewrite length_compute.
destruct (single_product_disjoint a X1 Y) as [[p1 p2] | [p1 p2]].
× rewrite p2.
destruct (a ∈_d X1).
** apply HX1.
** contradiction false_ne_true.
× rewrite p1, length_disjoint, HX1 ; try assumption.
rewrite length_singleproduct.
reflexivity.
Defined.
End length_product.
Section length_sum.
Context `{Univalence}.
Lemma length_fmap_inj
{A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}
(X : FSet A) (f : A → B) `{IsEmbedding f}
: length (fset_fmap f X) = length X.
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _ X)
; try (intros ; apply path_ishprop) ; simpl.
- reflexivity.
- intros a Y HX.
rewrite ?length_compute, HX, (fmap_isIn_d_inj _ f)
; auto.
Defined.
Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}.
Lemma fmap_inl X a : (inl a) ∈_d (fset_fmap (@inr A B) X) = false.
Proof.
hinduction X ; try (intros ; apply path_ishprop).
- reflexivity.
- intros b.
rewrite singleton_isIn_d_false.
× reflexivity.
× apply inl_ne_inr.
- intros X1 X2 HX1 HX2.
rewrite union_isIn_d, HX1, HX2.
reflexivity.
Defined.
Lemma fmap_inr X a : (inr a) ∈_d (fset_fmap (@inl A B) X) = false.
Proof.
hinduction X ; try (intros ; apply path_ishprop).
- reflexivity.
- intros b.
rewrite singleton_isIn_d_false.
× reflexivity.
× apply inr_ne_inl.
- intros X1 X2 HX1 HX2.
rewrite union_isIn_d, HX1, HX2.
reflexivity.
Defined.
Lemma disjoint_summants X Y : disjoint (fset_fmap (@inl A B) X) (fset_fmap inr Y).
Proof.
apply ext.
intros [x1 | x2] ; rewrite empty_isIn_d, intersection_isIn_d, ?fmap_inl, ?fmap_inr
; simpl ; try reflexivity.
destruct ((inl x1) ∈_d (fset_fmap inl X)) ; reflexivity.
Defined.
Open Scope nat.
Theorem length_disjoint_sum (X : FSet A) (Y : FSet B)
: length (disjoint_sum X Y) = length X + length Y.
Proof.
rewrite (length_disjoint _ _ (disjoint_summants _ _)).
rewrite ?(length_fmap_inj _ _).
reflexivity.
Defined.
End length_sum.
Section length_zero_one.
Context {A : Type} `{Univalence} `{MerelyDecidablePaths A}.
Lemma Z_not_S n : S n = 0 → Empty.
Proof.
refine (@equiv_path_nat (n.+1) 0)^-1.
Defined.
Lemma remove_S n m : S n = S m → n = m.
Proof.
intros X.
enough (n.+1 =n m.+1) as X0.
{
simpl in X0.
apply (equiv_path_nat X0).
}
apply ((equiv_path_nat)^-1 X).
Defined.
Theorem length_zero : ∀ (X : FSet A) (HX : length X = 0), X = ∅.
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _)
; try (intros ; apply path_ishprop) ; simpl.
- reflexivity.
- intros a X HX HaX.
rewrite length_compute in HaX.
unfold member_dec, fset_member_bool in HaX.
destruct (dec (a ∈ X)).
× pose (HX HaX) as XE.
pose (transport (fun Z ⇒ a ∈ Z) XE t) as Nonsense.
contradiction Nonsense.
× contradiction (Z_not_S _ HaX).
Defined.
Theorem length_one : ∀ (X : FSet A) (HX : length X = 1), hexists (fun a ⇒ X = {|a|}).
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _)
; try (intros ; apply path_ishprop) ; simpl.
- intros.
contradiction (Z_not_S _ (HX^)).
- intros a X HX HaX.
refine (tr(a;_)).
rewrite length_compute in HaX.
unfold member_dec, fset_member_bool in HaX.
destruct (dec (a ∈ X)).
× specialize (HX HaX).
strip_truncations.
destruct HX as [b HX].
assert (({|a|} : FSet A) = {|b|}) as p.
{
rewrite HX in t.
strip_truncations.
f_ap.
}
rewrite HX, p.
apply union_idem.
× rewrite (length_zero _ (remove_S _ _ HaX)).
apply nr.
Defined.
End length_zero_one.
Definition length_singleton a : length {|a|} = 1 := idpath.
Lemma length_compute (a : A) (X : FSet A) :
length ({|a|} ∪ X) = if (a ∈_d X) then length X else S(length X).
Proof.
unfold length.
rewrite FSet_cons_beta_cons.
reflexivity.
Defined.
Definition length_add (a : A) (X : FSet A) (p : a ∈_d X = false)
: length ({|a|} ∪ X) = 1 + (length X).
Proof.
rewrite length_compute.
destruct (a ∈_d X).
- contradiction (true_ne_false).
- reflexivity.
Defined.
Definition disjoint X Y := X ∩ Y = ∅.
Lemma disjoint_difference X Y : disjoint X (difference Y X).
Proof.
apply ext.
intros a.
rewrite intersection_isIn_d, empty_isIn_d, difference_isIn_d.
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
Defined.
Lemma disjoint_sub a X Y (H1 : disjoint ({|a|} ∪ X) Y) : disjoint X Y.
Proof.
unfold disjoint in ×.
apply ext.
intros b.
simplify_isIn_d.
rewrite empty_isIn_d.
pose (ap (fun Z ⇒ b ∈_d Z) H1) as p.
simpl in p.
rewrite intersection_isIn_d, empty_isIn_d, union_isIn_d in p.
destruct (b ∈_d X), (b ∈_d Y) ; try reflexivity.
- destruct (b ∈_d {|a|}) ; simpl in × ; try (contradiction true_ne_false).
Defined.
Definition length_disjoint (X Y : FSet A) :
∀ (HXY : disjoint X Y),
length (X ∪ Y) = (length X) + (length Y).
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _ X)
; try (intros ; apply path_ishprop) ; simpl.
- intros.
apply (ap length (nl _)).
- intros a X1 HX1 HX1Y.
rewrite <- assoc, ?length_compute, ?union_isIn_d in ×.
pose (ap (fun Z ⇒ a ∈_d Z) HX1Y) as p.
simpl in p.
rewrite intersection_isIn_d, union_isIn_d, singleton_isIn_d_aa, empty_isIn_d in p.
assert (orb (a ∈_d X1) (a ∈_d Y) = a ∈_d X1) as HaY.
{ destruct (a ∈_d X1), (a ∈_d Y) ; try reflexivity.
contradiction true_ne_false.
}
rewrite ?HaY, HX1.
destruct (a ∈_d X1) ; try reflexivity.
apply (disjoint_sub a X1 Y HX1Y).
Defined.
Lemma set_as_difference X Y : X = (difference X Y) ∪ (X ∩ Y).
Proof.
toBool.
generalize (a ∈_d X), (a ∈_d Y).
intros b c ; destruct b, c ; reflexivity.
Defined.
Lemma length_single_disjoint (X Y : FSet A) :
length X = length (difference X Y) + length (X ∩ Y).
Proof.
refine (ap length (set_as_difference X Y) @ _).
apply length_disjoint.
apply ext.
intros a.
rewrite ?intersection_isIn_d, empty_isIn_d, difference_isIn_d.
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
Defined.
Lemma union_to_disjoint X Y : X ∪ Y = X ∪ (difference Y X).
Proof.
toBool.
generalize (a ∈_d X), (a ∈_d Y).
intros b c ; destruct b, c ; reflexivity.
Defined.
Lemma length_union_1 (X Y : FSet A) :
length (X ∪ Y) = length X + length (difference Y X).
Proof.
refine (ap length (union_to_disjoint X Y) @ _).
apply length_disjoint.
apply ext.
intros a.
rewrite ?intersection_isIn_d, empty_isIn_d, difference_isIn_d.
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
Defined.
Lemma plus_assoc n m k : n + (m + k) = (n + m) + k.
Proof.
induction n ; simpl.
- reflexivity.
- rewrite IHn.
reflexivity.
Defined.
Lemma inclusion_exclusion (X Y : FSet A) :
length (X ∪ Y) + length (Y ∩ X) = length X + length Y.
Proof.
rewrite length_union_1.
rewrite (length_single_disjoint Y X).
rewrite plus_assoc.
reflexivity.
Defined.
End length.
Section length_product.
Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B} `{Univalence}.
Theorem length_singleproduct (a : A) (X : FSet B)
: length (single_product a X) = length X.
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _ X)
; try (intros ; apply path_ishprop) ; simpl.
- reflexivity.
- intros b X1 HX1.
rewrite ?length_compute, ?HX1.
enough(b ∈_d X1 = (a, b) ∈_d (single_product a X1)) as HE.
{ rewrite HE ; reflexivity. }
rewrite singleproduct_isIn_d_aa ; try reflexivity.
Defined.
Open Scope nat.
Lemma single_product_disjoint (a : A) (X1 : FSet A) (Y : FSet B)
: sum (prod (a ∈_d X1 = true)
((single_product a Y) ∪ (product X1 Y) = (product X1 Y)))
(prod (a ∈_d X1 = false)
(disjoint (single_product a Y) (product X1 Y))).
Proof.
pose (b := a ∈_d X1).
assert (a ∈_d X1 = b) as HaX1.
{ reflexivity. }
destruct b.
× refine (inl(HaX1,_)).
apply ext.
intros [a1 b1].
rewrite ?union_isIn_d.
unfold member_dec, fset_member_bool in ×.
destruct (dec ((a1, b1) ∈ (single_product a Y))) as [t | t]
; destruct (dec ((a1, b1) ∈ (product X1 Y))) as [p | p]
; try reflexivity.
rewrite singleproduct_isIn in t.
destruct t as [t1 t2].
rewrite product_isIn in p.
strip_truncations.
rewrite <- t1 in HaX1.
destruct (dec (a1 ∈ X1)) ; try (contradiction false_ne_true).
contradiction (p(t,t2)).
× refine (inr(HaX1,_)).
apply ext.
intros [a1 b1].
rewrite intersection_isIn_d, empty_isIn_d.
unfold member_dec, fset_member_bool in ×.
destruct (dec ((a1, b1) ∈ (single_product a Y))) as [t | t]
; destruct (dec ((a1, b1) ∈ (product X1 Y))) as [p | p]
; try reflexivity.
rewrite singleproduct_isIn in t ; destruct t as [t1 t2].
rewrite product_isIn in p ; destruct p as [p1 p2].
strip_truncations.
rewrite t1 in p1.
destruct (dec (a ∈ X1)).
** contradiction true_ne_false.
** contradiction (n p1).
Defined.
Theorem length_product (X : FSet A) (Y : FSet B)
: length (product X Y) = length X × length Y.
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _ X)
; try (intros ; apply path_ishprop) ; simpl.
- reflexivity.
- intros a X1 HX1.
rewrite length_compute.
destruct (single_product_disjoint a X1 Y) as [[p1 p2] | [p1 p2]].
× rewrite p2.
destruct (a ∈_d X1).
** apply HX1.
** contradiction false_ne_true.
× rewrite p1, length_disjoint, HX1 ; try assumption.
rewrite length_singleproduct.
reflexivity.
Defined.
End length_product.
Section length_sum.
Context `{Univalence}.
Lemma length_fmap_inj
{A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}
(X : FSet A) (f : A → B) `{IsEmbedding f}
: length (fset_fmap f X) = length X.
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _ X)
; try (intros ; apply path_ishprop) ; simpl.
- reflexivity.
- intros a Y HX.
rewrite ?length_compute, HX, (fmap_isIn_d_inj _ f)
; auto.
Defined.
Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}.
Lemma fmap_inl X a : (inl a) ∈_d (fset_fmap (@inr A B) X) = false.
Proof.
hinduction X ; try (intros ; apply path_ishprop).
- reflexivity.
- intros b.
rewrite singleton_isIn_d_false.
× reflexivity.
× apply inl_ne_inr.
- intros X1 X2 HX1 HX2.
rewrite union_isIn_d, HX1, HX2.
reflexivity.
Defined.
Lemma fmap_inr X a : (inr a) ∈_d (fset_fmap (@inl A B) X) = false.
Proof.
hinduction X ; try (intros ; apply path_ishprop).
- reflexivity.
- intros b.
rewrite singleton_isIn_d_false.
× reflexivity.
× apply inr_ne_inl.
- intros X1 X2 HX1 HX2.
rewrite union_isIn_d, HX1, HX2.
reflexivity.
Defined.
Lemma disjoint_summants X Y : disjoint (fset_fmap (@inl A B) X) (fset_fmap inr Y).
Proof.
apply ext.
intros [x1 | x2] ; rewrite empty_isIn_d, intersection_isIn_d, ?fmap_inl, ?fmap_inr
; simpl ; try reflexivity.
destruct ((inl x1) ∈_d (fset_fmap inl X)) ; reflexivity.
Defined.
Open Scope nat.
Theorem length_disjoint_sum (X : FSet A) (Y : FSet B)
: length (disjoint_sum X Y) = length X + length Y.
Proof.
rewrite (length_disjoint _ _ (disjoint_summants _ _)).
rewrite ?(length_fmap_inj _ _).
reflexivity.
Defined.
End length_sum.
Section length_zero_one.
Context {A : Type} `{Univalence} `{MerelyDecidablePaths A}.
Lemma Z_not_S n : S n = 0 → Empty.
Proof.
refine (@equiv_path_nat (n.+1) 0)^-1.
Defined.
Lemma remove_S n m : S n = S m → n = m.
Proof.
intros X.
enough (n.+1 =n m.+1) as X0.
{
simpl in X0.
apply (equiv_path_nat X0).
}
apply ((equiv_path_nat)^-1 X).
Defined.
Theorem length_zero : ∀ (X : FSet A) (HX : length X = 0), X = ∅.
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _)
; try (intros ; apply path_ishprop) ; simpl.
- reflexivity.
- intros a X HX HaX.
rewrite length_compute in HaX.
unfold member_dec, fset_member_bool in HaX.
destruct (dec (a ∈ X)).
× pose (HX HaX) as XE.
pose (transport (fun Z ⇒ a ∈ Z) XE t) as Nonsense.
contradiction Nonsense.
× contradiction (Z_not_S _ HaX).
Defined.
Theorem length_one : ∀ (X : FSet A) (HX : length X = 1), hexists (fun a ⇒ X = {|a|}).
Proof.
simple refine (FSet_cons_ind (fun Z ⇒ _) _ _ _ _ _)
; try (intros ; apply path_ishprop) ; simpl.
- intros.
contradiction (Z_not_S _ (HX^)).
- intros a X HX HaX.
refine (tr(a;_)).
rewrite length_compute in HaX.
unfold member_dec, fset_member_bool in HaX.
destruct (dec (a ∈ X)).
× specialize (HX HaX).
strip_truncations.
destruct HX as [b HX].
assert (({|a|} : FSet A) = {|b|}) as p.
{
rewrite HX in t.
strip_truncations.
f_ap.
}
rewrite HX, p.
apply union_idem.
× rewrite (length_zero _ (remove_S _ _ HaX)).
apply nr.
Defined.
End length_zero_one.