proposition: Lemma inject_term_eq : forall f ts (H : max_le (Fun f ts)), inject_term H = BFun f (inject_terms (maxvar_le_fun H)).
proof: Proof. intros. simpl. auto. Qed.
imports: CoLoR(ATerm VecUtil AInterpretation LogicUtil NatUtil)