proposition: Lemma inclusion_optimal_gonthier : extends E optimal gonthier.
proof: Proof. Proof using HE. split; simpl. auto. introv Dx. unfold optimal in *. epsilon g in Dx. apply~ optimal_fixed_point_exists. clearbody g. intros ((Gp&Gc)&Gu). epsilon g'. exists~ g (dom g). intros (D'&D'x&Gp'). clearbody g'. applys~ (Gc (Build_partial g' D')). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)