proposition: Lemma fsub_dom x0 n : forall ts : terms n, dom_incl (fsub x0 ts) (freshl (x0+1) n).
proof: Proof. unfold dom_incl. induction ts; simpl; intros. apply fsub_nil. split_all. ded (in_freshl H0). destruct H1. apply fsub_inf. lia. apply fsub_sup. lia. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)