proposition: Lemma sum_bl {A B eq_A eq_B} (A_bl : forall x y : A, eq_A x y = true -> x = y) (B_bl : forall x y : B, eq_B x y = true -> x = y) {x y} : sum_beq eq_A eq_B x y = true -> x = y.
proof: Proof. apply internal_sum_dec_bl; assumption. 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