fact: Definition sum_code (x y : A + B) : Prop := match x, y with | inl x', inl y' => x' = y' | inr x', inr y' => x' = y' | _, _ => False end.
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