fact: Definition extension_2 f fi := forall ix iy x y, contains (convert ix) x -> contains (convert iy) y -> contains (convert (fi ix iy)) (f x y).
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval