proposition: Lemma wf_subterm : well_founded subterm.
proof: Proof. red in |- *. simple induction a; intros; apply Acc_intro; intros. inversion_clear H; inversion_clear H0. inversion_clear H; inversion_clear H0. inversion_clear H1; inversion_clear H2; auto with coc sets. inversion_clear H1; inversion_clear H2; auto with coc sets. inversion_clear H1; inversion_clear H2; auto with coc sets. Qed.
imports: Peano_dec Transitive_Closure Union Termes Conv