proposition: Lemma projection_list_of_SN_terms : forall l proof, map tt (build_list_of_SN_terms l proof) = l.
proof: Proof. intro l; induction l; simpl; trivial. intros proof; apply (f_equal (fun l => a :: l)); apply IHl. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term