proposition: Lemma IAbs_strext : forall x y : subset I, AbsIR (f x) [#] AbsIR (f y) -> x [#] y.
proof: Proof. intros x y H. apply csf_strext_unfolded with (IR:CSetoid) f. simpl in H; unfold ABSIR in H; elim (bin_op_strext_unfolded _ _ _ _ _ _ H). auto. intro; apply un_op_strext_unfolded with (cg_inv (c:=IR)); assumption. Qed.
imports: CoRN.ftc.PartFunEquality