proposition: Theorem comp_state_eq_refl : forall (A : Set)(c : comp_state A), comp_state_eq c c.
proof: Proof. destruct c; intuition; econstructor. eapply Comp_eq_refl. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia