proposition: Lemma buildAbs_absType : forall a, absType (buildAbs_isAbs a) = a.(absT).
proof: Proof. destruct a as [[env ???] ??]; destruct env. try_solve. destruct o; try_solve. unfold VarD in * . inversion envNotEmpty0; trivial. Qed.
imports: CoLoR(RelExtras ListExtras LogicUtil) Coq(Lia)