From mathcomp Require Export ssreflect.
From iris.prelude Require Export prelude.
Set Default Proof Using "Type*".
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.