proposition: Lemma varD_UD_absurd : forall E p A, E |= p := A -> E |= p :! -> False.
proof: Proof. intros E p A EpA Ep. destruct Ep; unfold VarD in *; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)