proposition: Lemma IL_weqb_sound : forall x y, IL.weqb x y = true -> x = y.
proof: Proof. eauto using Word.weqb_sound. Qed.
imports: Bedrock.Platform.Cito.StringMap Bedrock.Platform.Cito.StringMapFacts Bedrock.Platform.Cito.SyntaxExpr Bedrock.Platform.Facade.DFacade Bedrock.Platform.Facade.DFacadeFacts2 Coq.Setoids.Setoid