proposition: Lemma in_sn_sn : forall l s, In s (map tt l) -> Acc rpo s.
proof: Proof. intro l; induction l. contradiction. intros s In_s; elim In_s; clear In_s; intro In_s. subst s; destruct a; trivial. apply IHl; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term