proposition: Theorem permutation_long_head : forall l1 l2 l3:list A, permutation l2 l3 -> permutation (l1 ++ l2) (l1 ++ l3).
proof: Proof. intros l1; elim l1; simpl in |- *; auto. intros a l1' Hrec l2 l3 H. constructor; auto. Qed.
imports: List Lia