proposition: Lemma In_fvs_Vnth : forall x n (ts : Tes n) i (h : i<n), In x (fv (Vnth ts h)) -> In x (fvs ts).
proof: Proof. intro x. induction ts; intros i hi. exfalso. lia. destruct i; simpl; set_iff. auto. intro a. right. eapply IHts. apply a. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)