proposition: Lemma pi_subterm : forall pi v1 v2 s t, axiom (Pi pi v1 v2) t s -> direct_subterm t s.
proof: Proof. intros pi v1 v2 s t H; inversion H as [t2' s' sigma H']; clear H; subst. inversion H' as [pi' H1 | pi' H2]; subst; simpl. left; trivial. right; left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)