proposition: Lemma lift_ltb_Irreflexiveb : forall x y, lift_eqb x y -> lift_ltb x y = false.
proof: Proof. unfold is_true, lift_ltb; intros x y H; rewrite H. edestruct lift_leb; simpl; congruence. Qed.
imports: Coq.FSets.FMapInterface Fiat.Common.Wf Fiat.Common.FMapExtensions Fiat.Common.FMapExtensions.LiftRelationInstances Fiat.Common