proposition: Lemma bool_bl {x y} : bool_beq x y = true -> x = y.
proof: Proof. apply internal_bool_dec_bl. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Common