fact: Definition lift_ltb (x y : t) : bool := ((subset x y) && negb (equal x y)).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.MSets.MSetInterface Coq.MSets.MSetFacts Coq.MSets.MSetProperties Fiat.Common.Wf Fiat.Common.LogicFacts Fiat.Common.Instances Fiat.Common.NatFacts Fiat.Common.MSetExtensions Fiat.Common