proposition: Lemma tri_proj_eq {A C D} : forall a c d (acd : A * C * D), a = fst (fst acd) -> c = snd (fst acd) -> d = snd acd -> acd = ((a, c), d).
proof: Proof. intros; subst; intuition. Qed.
imports: Fiat.Common.ilist Fiat.Common.SumType Fiat.Common.IterateBoundedIndex Fiat.Narcissus.Common.Specs Coq.Sets.Ensembles Bedrock.Word