proposition: Lemma subterm_pos_replace_neq_None : forall p u v t, subterm_pos t p = Some u -> replace_pos t p v <> None.
proof: Proof. intros. destruct (subterm_pos_replace_eq_Some p v t H). rewrite e. discr. Qed.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)