proposition: Theorem test_compat_l: forall a b c, test a b = eq -> test a c = test b c.
proof: Proof. intros a; elim a; simpl; auto; clear a. intros b; case b; try (intros; discriminate; fail). intros c; case c; auto. intros a Rec b; case b; clear b. intros; discriminate. intros b c Hb; case c; simpl; auto. Qed.
imports: List Permutation UList