fact: Definition Fix A {IA:Inhab A} (E C:binary A) (F:A->A) : A := epsilon (Fix_prop E C F).
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)