proposition: Lemma Permutation_reord i ll1 l1 a b l2 ll2 : Permutation (i ++ concat (ll1 ++ (l1 ++ b :: a :: l2) :: ll2)) (i ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)).
proof: Proof. Proof using. rewrite !concat_app, !concat_cons; ins; eauto using Permutation_app, perm_swap. Qed.
imports: HahnBase HahnList HahnRelationsBasic