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