proposition: Lemma Permutation_app_head : forall (l tl tl' : list A), Permutation tl tl' -> Permutation (l++tl) (l++tl').
proof: Proof. intros l tl tl' Hperm; induction l; [trivial | repeat rewrite <- app_comm_cons; constructor; assumption]. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat