proposition: Lemma subterm_trans_eq2 : forall t u v, subterm t u -> subterm_eq u v -> subterm t v.
proof: Proof. unfold subterm, subterm_eq. intros. destruct H. destruct H. destruct H0. subst u. subst v. rewrite (fill_fill x0 x t). exists (comp x0 x). split. destruct x. cong. destruct x0; simpl; discr. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)