proposition: Lemma reghost_deghost_partial_inverses : forall net, deghost (reghost net) = net.
proof: Proof. Proof using. destruct net. unfold deghost, reghost. simpl in *. f_equal. rewrite map_map. map_id. Qed.
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)