proposition: Lemma permut_length_2 : forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] -> (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
proof: Proof. intros a1 b1 a2 b2 P. assert (H:=permut_cons_InA P). inversion_clear H. - left; split; auto. apply permut_length_1. red; red; intros. specialize (P a). simpl in *. rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. lia. - right. inversion_clear H0; [|inversion H]. split; auto. apply permut_length_1. red; red; intros. specialize (P a); simpl in *. rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. lia. Qed.
imports: Lia Relations Multiset SetoidList