proposition: Lemma getAllBlists_rel_map : forall n, rel_map (fun ls1 ls2 => ls1 = (rev ls2)) (getAllBlists n) (getAllBlists_app n).
proof: Proof. induction n; intuition; simpl in *. econstructor. econstructor. trivial. eapply rel_map_app. eapply rel_map_map2. eapply rel_map_impl; eauto; intuition. subst. rewrite rev_unit. trivial. eapply rel_map_map2. eapply rel_map_impl; eauto; intuition. subst. rewrite rev_unit. trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation