proposition: Lemma absorb_strict : absorbs_left R E.
proof: Proof. unfold absorbs_left, inclusion, RelUtil.compose, strict_part. intros; split; decomp H. eapply E_trans. apply H1. hyp. unfold not; intro. ded (E_trans H H1). contr. Qed.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)