proposition: Lemma subterm_size : forall t u : term, subterm t u -> size t < size u.
proof: Proof. intros t u [C [hC e]]. subst u. destruct C. cong. simpl fill. rewrite size_fun, size_terms_cast, size_terms_app. simpl. ded (size_fill t C). lia. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)