proposition: Lemma var_notin_ok xs : ~In (var_notin xs) xs.
proof: Proof. unfold var_notin. case_eq (max_elt xs). intros k e h. gen (max_elt_2 e h). lia. intro h. apply max_elt_3 in h. fo. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)