Add proj-of-prop soundness test

tests/proj-of-prop.lean

@@ -0,0 +1,30 @@
+import Lean
+open Lean Elab Command
+
+structure Wrapper : Prop where
+  mk ::
+  p : False
+
+/-
+The value we want to add is
+
+    Expr.proj `Wrapper 0 (Wrapper.mk True.intro)
+
+which has a `True.intro : True` sitting in the `Wrapper.mk` slot that
+expects a `False`. The elaborator never emits a raw `Expr.proj` from
+`(...).p` syntax (it desugars to the projection *function* `Wrapper.p`,
+which would get caught at `infer_app`), so we construct the declaration
+programmatically and hand it to `addDecl` under `debug.skipKernelTC`.
+-/
+
+run_cmd liftTermElabM do
+  let badValue : Expr :=
+    .proj `Wrapper 0 (mkApp (mkConst ``Wrapper.mk) (mkConst ``True.intro))
+  let decl : Declaration := .thmDecl {
+    name        := `badFalse
+    levelParams := []
+    type        := mkConst ``False
+    value       := badValue
+  }
+  withOptions (debug.skipKernelTC.set · true) do
+    addDecl decl

tests/proj-of-prop.yaml

@@ -0,0 +1,19 @@
+description: |
+  A proof of `False` via a projection from a `Prop`-typed structure whose
+  constructor was applied to an ill-typed argument. The exported term is
+
+      badFalse : False := (Wrapper.mk True.intro).p
+
+  where `Wrapper : Prop` has a single field `p : False`, so `Wrapper.mk`
+  expects a proof of `False` but is given `True.intro : True`.
+
+  A sound checker must reject this. A checker that types a projection by
+  inferring (rather than checking) its structure argument — i.e. that
+  trusts the structure to be well-typed instead of verifying the
+  constructor's argument types against its binders — will accept it,
+  because `Wrapper.mk True.intro` still formally inhabits `Wrapper` at
+  the structural level, and the `p` projection is then read back out at
+  the declared field type `False`.
+leanfile: tests/proj-of-prop.lean
+export-decls: ["badFalse"]
+outcome: reject