proposition: Theorem test_anti_sym: forall n1 n2, test n1 n2 = opp (test n2 n1).
proof: Proof. intros n1; elim n1; simpl; auto; clear n1. intros n2; elim n2; simpl; auto; clear n2. intros n1 Rec n2; elim n2; simpl; auto; clear n2. Qed.
imports: List Permutation UList