proposition: Lemma permut_length_2 : forall (A B : Type) (R : A -> B -> Prop) a1 b1 a2 b2, permut0 R (a1 :: b1 :: nil) (a2 :: b2 :: nil) -> (R a1 a2 /\ R b1 b2) \/ (R a1 b2 /\ R b1 a2).
proof: Proof. intros A B R a1 b1 a2 b2 P; inversion P as [ | a b l l1 l2 a_R_b P' H1 H']; subst. destruct l1 as [ | c1 l1]. destruct l2 as [ | c2 [ | d2 l2]]. discriminate. injection H'; intros; subst. left; split; trivial. apply (permut_length_1 P'). discriminate. destruct l1 as [ | d1 l1]. destruct l2 as [ | c2 l2]. injection H'; intros; subst. right; split; trivial. apply (permut_length_1 P'). discriminate. destruct l1; discriminate. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)