nominal register_a = ()
nominal slot0 = ()
nominal slot1 = ()
nominal coherent = ()
union qubit register slot phase = | Qubit :: forall register slot phase. string -> qubit register slot phase
union distinct left right = | Slot0Slot1 :: distinct slot0 slot1
inl cnot forall register control target. (control : qubit register control coherent) (target : qubit register target coherent) (proof : distinct control target) : qubit register control coherent * qubit register target coherent = control, target
inl main () =
    inl qubit : qubit register_a slot0 coherent = Qubit "q0"
    cnot qubit qubit Slot0Slot1