fact: Definition Fkont_equiv `(M : @EMonoid A op E_one E_equiv) (k k': Fkont A ) := forall x y : A, x == y -> computation_equiv op E_equiv (k x) (k' y).
imports: Coq(Inverse_Image Inclusion Wf_nat NArith Arith PArith Recdef Wf_nat Lexicographic_Product Lia) additions(Addition_Chains Compatibility More_on_positive Wf_transparent Dichotomy BinaryStrat) Coq(Lia)