proposition: Lemma tot_map_trace_occ_in_inv : forall tr h inp out, map tot_map_trace_occ tr = [(h, inl inp); (h, inr out)] -> exists h', exists inp', exists out', tr = [(h', inl inp'); (h', inr out')] /\ tot_map_name h' = h /\ map tot_map_output out' = out /\ tot_map_input inp' = inp.
proof: Proof. Proof using name_map_bijective. case => //=. case. move => h. case => //. move => inp. case => //. case. move => h'. case => //. move => out. case => //=. move => h0. move => inp' out' H_eq. inversion H_eq. find_apply_lem_hyp tot_map_name_injective. repeat find_rewrite. by exists h; exists inp; exists out. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)