proposition: Lemma empty_ltb_nothing v : lift_ltb (empty _) v = false.
proof: Proof. unfold lift_ltb. apply not_true_iff_false, BoolFacts.not_andb_negb_iff. unfold lift_leb, lift_eqb. setoid_rewrite lift_brelation_iff. intros H k; specialize (H k). rewrite empty_o in *. edestruct find; [ | reflexivity ]. apply top_eqb; assumption. Qed.
imports: Coq.FSets.FMapInterface Fiat.Common.Wf Fiat.Common.FMapExtensions Fiat.Common.FMapExtensions.LiftRelationInstances Fiat.Common