theorem Iris.Tests.start_stop {PROP : Type u_1} [BI PROP] (Q : PROP) (H : Q ⊢ Q) : Q ⊢ Q

theorem Iris.Tests.rename.rename {PROP : Type u_1} [BI PROP] (Q : PROP) : Q ⊢ Q

theorem Iris.Tests.rename.rename_by_type {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ P ∗ Q ⊢ Q

theorem Iris.Tests.rename.rename_twice {PROP : Type u_1} [BI PROP] (Q : PROP) : Q ⊢ Q

theorem Iris.Tests.rename.rename_id {PROP : Type u_1} [BI PROP] (Q : PROP) : Q ⊢ Q

theorem Iris.Tests.clear.intuitionistic {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ P ⊢ Q -∗ Q

theorem Iris.Tests.clear.spatial {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : <affine> P ⊢ Q -∗ Q

theorem Iris.Tests.intro.spatial {PROP : Type u_1} [BI PROP] (Q : PROP) : Q ⊢ Q

theorem Iris.Tests.intro.intuitionistic {PROP : Type u_1} [BI PROP] (Q : PROP) : □ Q ⊢ Q

theorem Iris.Tests.intro.as_intuitionistic {PROP : Type u_1} [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ Q

theorem Iris.Tests.intro.as_intuitionistic_in_spatial {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ <pers> Q → Q

theorem Iris.Tests.intro.drop {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : ⊢ P → Q -∗ Q

theorem Iris.Tests.intro.drop_after {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : ⊢ Q -∗ P → Q

theorem Iris.Tests.intro.forall {PROP : Type u_1} [BI PROP] : ⊢ BI.forall fun (x : Nat) => iprop(⌜x = 0⌝ → ⌜x = 0⌝)

theorem Iris.Tests.intro.pure {PROP : Type u_1} {φ : Prop} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : ⊢ ⌜φ⌝ -∗ Q -∗ Q

theorem Iris.Tests.intro.pattern {PROP : Type u_1} {P1 P2 : PROP} [BI PROP] (Q : PROP) : □ (P1 ∨ P2) ∗ Q ⊢ Q

theorem Iris.Tests.intro.multiple_spatial {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : ⊢ <affine> P -∗ Q -∗ Q

theorem Iris.Tests.intro.multiple_intuitionistic {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : ⊢ □ P -∗ □ Q -∗ Q

theorem Iris.Tests.intro.multiple_patterns {PROP : Type u_1} {P1 P2 : PROP} [BI PROP] (Q : PROP) : ⊢ □ (P1 ∧ P2) -∗ Q ∨ Q -∗ Q

theorem Iris.Tests.exists.id {PROP : Type u_1} [BI PROP] : ⊢ BI.exists fun (x : PROP) => x

theorem Iris.Tests.exists.f {PROP : Type u_1} [BI PROP] : ⊢ BI.exists fun (_x : Nat) => iprop(True ∨ False)

theorem Iris.Tests.exists.pure {PROP : Type u_1} [BI PROP] : ⊢ ⌜∃ (x : Prop), x ∨ False⌝

theorem Iris.Tests.exact.exact {PROP : Type u_1} [BI PROP] (Q : PROP) : Q ⊢ Q

theorem Iris.Tests.exact.def_eq {PROP : Type u_1} [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q

theorem Iris.Tests.exact.intuitionistic {PROP : Type u_1} [BI PROP] (Q : PROP) : □ Q ⊢ Q

theorem Iris.Tests.assumption.exact {PROP : Type u_1} [BI PROP] (Q : PROP) : Q ⊢ Q

theorem Iris.Tests.assumption.from_assumption {PROP : Type u_1} [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q

theorem Iris.Tests.assumption.intuitionistic {PROP : Type u_1} [BI PROP] (Q : PROP) : □ Q ⊢ Q

theorem Iris.Tests.assumption.lean {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) (H : ⊢ Q) : <affine> P ⊢ Q

theorem Iris.Tests.assumption.lean_pure {PROP : Type u_1} [BI PROP] (Q : PROP) : <affine> ⌜⊢ Q⌝ ⊢ Q

theorem Iris.Tests.exfalso.false_intro {PROP : Type u_1} [BI PROP] (Q : PROP) : False ⊢ Q

theorem Iris.Tests.exfalso.false {PROP : Type u_1} {Q : PROP} [BI PROP] (P : PROP) : □ P ⊢ False -∗ Q

theorem Iris.Tests.exfalso.pure {PROP : Type u_1} [BI PROP] (P : PROP) (HF : False) : ⊢ P

theorem Iris.Tests.pure.move {PROP : Type u_1} {φ : Prop} [BI PROP] (Q : PROP) : <affine> ⌜φ⌝ ⊢ Q -∗ Q

theorem Iris.Tests.pure.move_multiple {PROP : Type u_1} {φ1 φ2 : Prop} [BI PROP] (Q : PROP) : <affine> ⌜φ1⌝ ⊢ <affine> ⌜φ2⌝ -∗ Q -∗ Q

theorem Iris.Tests.pure.move_conjunction {PROP : Type u_1} {φ1 φ2 : Prop} [BI PROP] (Q : PROP) : ⌜φ1⌝ ∧ <affine> ⌜φ2⌝ ⊢ Q -∗ Q

theorem Iris.Tests.intuitionistic.move {PROP : Type u_1} {Q : PROP} [BI PROP] (P : PROP) : □ P ⊢ Q -∗ Q

theorem Iris.Tests.intuitionistic.move_multiple {PROP : Type u_1} {Q : PROP} [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q

theorem Iris.Tests.intuitionistic.move_twice {PROP : Type u_1} {Q : PROP} [BI PROP] (P : PROP) : □ P ⊢ Q -∗ Q

theorem Iris.Tests.spatial.move {PROP : Type u_1} {Q : PROP} [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q

theorem Iris.Tests.spatial.move_multiple {PROP : Type u_1} {Q : PROP} [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q

theorem Iris.Tests.spatial.move_twice {PROP : Type u_1} {Q : PROP} [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q

theorem Iris.Tests.empintro.simple {PROP : Type u_1} [BI PROP] : ⊢ emp

theorem Iris.Tests.empintro.affine_env {PROP : Type u_1} [BI PROP] (P : PROP) : <affine> P ⊢ emp

theorem Iris.Tests.pureintro.simple {PROP : Type u_1} [BI PROP] : ⊢ True

theorem Iris.Tests.pureintro.or {PROP : Type u_1} [BI PROP] : ⊢ True ∨ False

theorem Iris.Tests.pureintro.with_proof {PROP : Type u_1} {A B : Prop} [BI PROP] (H : A → B) (P Q : PROP) : <affine> P ⊢ <pers> Q → ⌜A⌝ → ⌜B⌝

theorem Iris.Tests.specialize.wand_spatial {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q

theorem Iris.Tests.specialize.wand_intuitionistic {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ □ Q

theorem Iris.Tests.specialize.wand_intuitionistic_overwrite {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ P ⊢ □ (□ P -∗ Q) -∗ □ Q

theorem Iris.Tests.specialize.wand_intuitionistic_required {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ P ⊢ □ (□ P -∗ Q) -∗ □ Q

theorem Iris.Tests.specialize.wand_intuitionistic_spatial {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ P ⊢ (P -∗ Q) -∗ Q

theorem Iris.Tests.specialize.wand_intuitionistic_required_spatial {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ P ⊢ (□ P -∗ Q) -∗ Q

theorem Iris.Tests.specialize.wand_spatial_intuitionistic {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : P ⊢ □ (P -∗ Q) -∗ Q

theorem Iris.Tests.specialize.wand_spatial_multiple {PROP : Type u_1} {P1 P2 : PROP} [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q

theorem Iris.Tests.specialize.wand_intuitionistic_multiple {PROP : Type u_1} {P1 P2 : PROP} [BI PROP] (Q : PROP) : ⊢ □ P1 -∗ □ P2 -∗ □ (P1 -∗ □ P2 -∗ Q) -∗ □ Q

theorem Iris.Tests.specialize.wand_multiple {PROP : Type u_1} {P1 P2 P3 : PROP} [BI PROP] (Q : PROP) : ⊢ P1 -∗ □ P2 -∗ P3 -∗ □ (P1 -∗ P2 -∗ P3 -∗ Q) -∗ Q

theorem Iris.Tests.specialize.forall_spatial {PROP : Type u_1} {y : Nat} [BI PROP] (Q : Nat → PROP) : ⊢ (BI.forall fun (x : Nat) => Q x) -∗ Q (y + 1)

theorem Iris.Tests.specialize.forall_intuitionistic {PROP : Type u_1} {y : Nat} [BI PROP] (Q : Nat → PROP) : ⊢ (□ BI.forall fun (x : Nat) => Q x) -∗ □ Q y

theorem Iris.Tests.specialize.forall_intuitionistic_overwrite {PROP : Type u_1} {y : Nat} [BI PROP] (Q : Nat → PROP) : ⊢ (□ BI.forall fun (x : Nat) => Q x) -∗ □ Q y

theorem Iris.Tests.specialize.forall_spatial_intuitionistic {PROP : Type u_1} {y : Nat} [BI PROP] (Q : Nat → PROP) : ⊢ (BI.forall fun (x : Nat) => iprop(□ Q x)) -∗ □ Q y

theorem Iris.Tests.specialize.forall_spatial_multiple {PROP : Type u_1} {x y : Nat} [BI PROP] (Q : Nat → Nat → PROP) : ⊢ (BI.forall fun (x : Nat) => BI.forall fun (y : Nat) => Q x y) -∗ Q x y

theorem Iris.Tests.specialize.forall_intuitionistic_multiple {PROP : Type u_1} {x y : Nat} [BI PROP] (Q : Nat → Nat → PROP) : ⊢ (□ BI.forall fun (x : Nat) => BI.forall fun (y : Nat) => Q x y) -∗ □ Q x y

theorem Iris.Tests.specialize.forall_multiple {PROP : Type u_1} {x y : Nat} [BI PROP] (Q : Nat → Nat → PROP) : ⊢ (BI.forall fun (x : Nat) => iprop(□ BI.forall fun (y : Nat) => Q x y)) -∗ □ Q x y

theorem Iris.Tests.specialize.multiple {PROP : Type u_1} {P1 P2 : PROP} {y : Nat} [BI PROP] (Q : Nat → PROP) : ⊢ □ P1 -∗ P2 -∗ (□ P1 -∗ BI.forall fun (x : Nat) => iprop(P2 -∗ Q x)) -∗ Q y

theorem Iris.Tests.split.and {PROP : Type u_1} [BI PROP] (Q : PROP) : Q ⊢ Q ∧ Q

theorem Iris.Tests.split.sep_left {PROP : Type u_1} {P R : PROP} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q

theorem Iris.Tests.split.sep_right {PROP : Type u_1} {P R : PROP} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q

theorem Iris.Tests.split.sep_left_all {PROP : Type u_1} {P R : PROP} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : ⊢ P -∗ □ Q -∗ R -∗ P ∗ Q

theorem Iris.Tests.split.sep_right_all {PROP : Type u_1} {P R : PROP} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : ⊢ □ P -∗ Q -∗ R -∗ P ∗ Q

theorem Iris.Tests.leftright.left {PROP : Type u_1} {Q : PROP} [BI PROP] (P : PROP) : P ⊢ P ∨ Q

theorem Iris.Tests.leftright.right {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : Q ⊢ P ∨ Q

theorem Iris.Tests.leftright.complex {PROP : Type u_1} {R : PROP} [BI PROP] (P Q : PROP) : ⊢ P -∗ Q -∗ P ∗ (R ∨ Q ∨ R)

theorem Iris.Tests.cases.rename {PROP : Type u_1} [BI PROP] (P : PROP) : P ⊢ P

theorem Iris.Tests.cases.clear {PROP : Type u_1} [BI PROP] (P Q : PROP) : ⊢ P -∗ <affine> Q -∗ P

theorem Iris.Tests.cases.and {PROP : Type u_1} {P1 P2 : PROP} [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q) ⊢ Q

theorem Iris.Tests.cases.and_intuitionistic {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ P ∧ Q ⊢ Q

theorem Iris.Tests.cases.and_persistent_left {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : <pers> Q ∧ <affine> P ⊢ Q

theorem Iris.Tests.cases.and_persistent_right {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : Q ∧ <pers> P ⊢ Q

theorem Iris.Tests.cases.sep {PROP : Type u_1} {P1 P2 : PROP} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : P1 ∗ P2 ∗ Q ⊢ Q

theorem Iris.Tests.cases.disjunction {PROP : Type u_1} {P1 P2 P3 : PROP} [BI PROP] (Q : PROP) : Q ⊢ <affine> (P1 ∨ P2 ∨ P3) -∗ Q

theorem Iris.Tests.cases.conjunction_and_disjunction {PROP : Type u_1} {P11 P12 P13 P2 P31 P32 P33 : PROP} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : (P11 ∨ P12 ∨ P13) ∗ P2 ∗ (P31 ∨ P32 ∨ P33) ∗ Q ⊢ Q

theorem Iris.Tests.cases.move_to_pure {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ <affine> ⌜⊢ Q⌝ -∗ Q

theorem Iris.Tests.cases.move_to_pure_ascii {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ <affine> ⌜⊢ Q⌝ -∗ Q

theorem Iris.Tests.cases.move_to_intuitionistic {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q

theorem Iris.Tests.cases.move_to_intuitionistic_ascii {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q

theorem Iris.Tests.cases.move_to_spatial {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q

theorem Iris.Tests.cases.move_to_spatial_ascii {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ □ Q -∗ Q

theorem Iris.Tests.cases.move_to_pure_conjunction {PROP : Type u_1} {φ : Prop} [BI PROP] (Q : PROP) : ⊢ <affine> ⌜φ⌝ ∗ Q -∗ Q

theorem Iris.Tests.cases.move_to_pure_disjunction {PROP : Type u_1} {φ1 φ2 : Prop} [BI PROP] (Q : PROP) : ⊢ <affine> ⌜φ1⌝ ∨ <affine> ⌜φ2⌝ -∗ Q -∗ Q

theorem Iris.Tests.cases.move_to_intuitionistic_conjunction {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : ⊢ □ P ∗ Q -∗ Q

theorem Iris.Tests.cases.move_to_intuitionistic_disjunction {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ □ Q ∨ Q -∗ Q

theorem Iris.Tests.cases.move_to_spatial_conjunction {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q

theorem Iris.Tests.cases.move_to_spatial_disjunction {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q

theorem Iris.Tests.cases.move_to_intuitionistic_and_back_conjunction {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q

theorem Iris.Tests.cases.move_to_intuitionistic_and_back_disjunction {PROP : Type u_1} [BI PROP] (Q : PROP) : ⊢ □ (Q ∨ Q) -∗ Q

theorem Iris.Tests.cases.conjunction_clear {PROP : Type u_1} {P : PROP} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : Q ∗ P ⊢ Q

theorem Iris.Tests.cases.disjunction_clear {PROP : Type u_1} {P1 P2 : PROP} [BI PROP] [BI.BIAffine PROP] (Q : PROP) : Q ⊢ P1 ∨ P2 -∗ Q

theorem Iris.Tests.cases.and_destruct_spatial_right {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : P ∧ Q ⊢ Q

theorem Iris.Tests.cases.and_destruct_spatial_left {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : Q ∧ P ⊢ Q

theorem Iris.Tests.cases.and_clear_spatial_multiple {PROP : Type u_1} {P1 P2 P3 : PROP} [BI PROP] (Q : PROP) : P1 ∧ P2 ∧ Q ∧ P3 ⊢ Q

theorem Iris.Tests.cases.and_destruct_intuitionistic_right {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ (P ∧ Q) ⊢ Q

theorem Iris.Tests.cases.and_destruct_intuitionistic_left {PROP : Type u_1} {P : PROP} [BI PROP] (Q : PROP) : □ (Q ∧ P) ⊢ Q

theorem Iris.Tests.cases.and_clear_intuitionistic_multiple {PROP : Type u_1} {P1 P2 P3 : PROP} [BI PROP] (Q : PROP) : □ (P1 ∧ P2 ∧ Q ∧ P3) ⊢ Q

theorem Iris.Tests.cases.exists {PROP : Type u_1} [BI PROP] (Q : Nat → PROP) : (BI.exists fun (x : Nat) => Q x) ⊢ BI.exists fun (x : Nat) => iprop(Q x ∨ False)

theorem Iris.Tests.cases.exists_intuitionistic {PROP : Type u_1} [BI PROP] (Q : Nat → PROP) : (□ BI.exists fun (x : Nat) => Q x) ⊢ BI.exists fun (x : Nat) => iprop(□ Q x ∨ False)