proposition: Lemma is_true_is_false_contradiction : forall av expr st, @is_true av expr st -> @is_false av expr st -> False.
proof: Proof. unfold is_true, is_false; intros; congruence. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.PureUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.FacadeUtils Coq.Setoids.Setoid