Lvc.Coherence.DelocationValidator

Require Import AllInRel Util Map Env EnvTy Exp IL Annotation Coherence Bisim DecSolve Liveness Restrict Delocation.

Set Implicit Arguments.

Lemma trs_dec DL ZL s ans_lv ans
  : {trs DL ZL s ans_lv ans} +
    {¬ trs DL ZL s ans_lv ans}.

Instance trs_dec_inst DL ZL s lv Y
: Computable (trs DL ZL s lv Y).