proposition: Lemma buildAbs_env : forall a, env (buildAbs a) = tail (env a.(absB)).
proof: Proof. destruct a as [[env ???] ??]; destruct env. try_solve. destruct o; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras LogicUtil) Coq(Lia)