proposition: Lemma repair : forall A B (x : A * B), (fst x, snd x) = x.
proof: Proof. destruct x; auto. Qed.
imports: Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildComputationalADT Fiat.ADTNotation.BuildADTSig Fiat.ADTRefinement.GeneralRefinements Fiat.Common.ilist Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.ADT.ComputationalADT Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.ADT.ComputationalADT Fiat.ADTRefinement.GeneralBuildADTRefinements Coq.Bool.Bool Coq.ZArith.ZArith