关于：projNonPropFromProp
当尝试使用命题证明投影一段数据时，会发生此错误
指数投影。例如，如果 h 是存在命题的证明，则尝试
提取见证 h.1 是此错误的一个示例。此类预测是不允许的，因为它们
可能违反 Lean 对 Prop 进行大消除的禁止（请参阅
Propositions 手册部分了解更多详细信息）。
考虑使用模式匹配而不是索引投影
Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let、Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 表达式或
像 cases 一样解构策略以从一种命题类型消除到另一种命题类型。注意事项
仅当结果值也在 Prop 中时，这种消除才有效；如果不是，
错误 lean.propRecLargeElim
将被提高。
示例
Attempting to Use Index Projection on Existential Proof
与存在命题的证明相关的证人不能使用以下方法提取：
指数投影。相反，有必要使用模式匹配：或者像 a 这样的术语
Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 绑定或策略（如 cases）。