proposition: Theorem fork_spec1 : forall A B e, fork↓e ⊩ A → B → (A ∩ B).
proof: Proof. Ksolve; [fork1 | fork2]; Ksolve. Qed.
imports: Arith Omega ClassicalRealizability.Kbase ClassicalRealizability.Integers ClassicalRealizability.KBool