proposition: Lemma V_or : forall x f, (inc (pair x (V x f)) f) \/ ((forall z, ~(inc (pair x z) f)) & (V x f = emptyset)).
proof: Proof. ir. apply by_cases with (ex (fun y=> inc (pair x y) f)). ir. ap or_introl. app V_inc. ir. ap or_intror. ee. ir. uhg; ee. ir. ap H. sh z; am. uf V. ap choose_not. am. Qed.
imports: tactics