proposition: Lemma dec_refl {A} (dec : forall x y : A, {x = y} + {x <> y}) x : dec x x = left eq_refl.
proof: Proof. edestruct dec; [ | congruence ]. apply f_equal, UIP_dec, dec. 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