| refl : \forall l:list A. permutation ? l l
| swap : \forall l:list A. \forall x,y:A.
permutation ? (x :: y :: l) (y :: x :: l)
| refl : \forall l:list A. permutation ? l l
| swap : \forall l:list A. \forall x,y:A.
permutation ? (x :: y :: l) (y :: x :: l)