proposition: Lemma opt_absorbs_right_opt_r E : R @ E << R -> opt @ opt_r E << opt.
proof: Proof. intros RE x z [y [xy yz]]. inversion xy; clear xy; subst. inversion yz; clear yz; subst. apply opt_intro. apply RE. exists y0. fo. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)