proposition: Lemma subterm_immediate : forall f v a, In a v -> subterm a (Fun f v).
proof: Proof. intros. destruct (In_split a v) as [l1 [l2 dec]]. hyp. exists (Cont f l1 Hole l2). split. discr. simpl. congruence. Qed.
imports: CoLoR(LogicUtil) CoLoR(ListUtil)