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