From stdpp Require Import binders strings stringmap.
From iris.base_logic Require Import lib.iprop.

Require Import lang.

Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ P.
    move=> Σ P Q.
    apply: (check_program_spec (Lam "x" (Var "x"))).
    rewrite /check_program; simpl.
    done.
Qed.

Goal ∀ {Σ} (P Q : iProp Σ), ⊢ P -∗ Q -∗ Q ∗ P.
    move=> Σ P Q.
    apply: (check_program_spec (Lam "x" (Lam "y" (Pair (Var "y") (Var "x"))))).
    rewrite /check_program; simpl.
    done.
Qed.