proposition: Lemma IL_weqb_refl : forall x, IL.weqb x x = true.
proof: Proof. unfold IL.weqb. intros; rewrite Word.weqb_true_iff; reflexivity. 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