idestruct_bench_2.v

From stdpp Require Import base.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import iprop.

Section S.
Context (Σ: gFunctors).

Lemma dup (P: Prop) : P -> P -> P. auto. Qed.

Ltac dup n :=
  lazymatch n with
  | O => idtac
  | S ?m => apply dup; [ dup m | dup m ]
  end.

Goal ∀ (A: iProp Σ),
    Persistent A →
    A -∗ False.
Proof.
  intros. iIntros "X".
  dup 10.
  all: iDestruct "X" as "#A".
Abort.

End S.