# Proof term: reading λh. ⟨snd h, fst h⟩ part by part as a proof term for P∧Q→Q∧P [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-lean-proof-term/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-lean-proof-term-01 · production-20261019-adopted-96 ## Goal and scope In an explicit synthetic small propositional type system ST (matching MKO assumption a2), with distinct propositional atoms P and Q: explain part by part what each piece of the term t=λh:P∧Q. ⟨snd h, fst h⟩ establishes and what type it has, derive the judgment ⊢ t : P∧Q→Q∧P, and explain why the type of t matches the proposition S=P∧Q→Q∧P; then prove that the similar-looking t′=λh:P∧Q. ⟨fst h, snd h⟩ is not a proof term for S. Finally separate three things: a typing derivation in ST, acceptance by the Lean kernel, and a saved proof-term receipt. Typing derivations are carried out only in the synthetic system ST, where type equality is syntactic identity; ST has none of Lean's definitional equality (conversion), universes, implicit arguments or elaboration. This guide does not run Lean, does not claim that any term has been compiled, elaborated or checked by Lean's kernel, and produces no Lean formal Evidence or receipt; the Lean 4 surface notation that appears is only a reading aid. It does not change the canonical MKO or its English edition. ## Givens and symbols - def_unfold - and_intro_elim - imp_intro - contradiction - G1 — The environment E_ST is fixed: P and Q are two distinct propositional atoms, each already given as a proposition (MKO assumption a1); types are built from atoms with ∧ and →. Terms, contexts and the rule table stay fixed throughout. - G2 — ST has exactly six rules. Var: if x:A is listed in Γ then Γ⊢x:A. ∧I: from Γ⊢a:A and Γ⊢b:B infer Γ⊢⟨a,b⟩:A∧B. ∧E1: from Γ⊢p:A∧B infer Γ⊢fst p:A. ∧E2: from Γ⊢p:A∧B infer Γ⊢snd p:B. →I: from Γ,x:A⊢b:B infer Γ⊢λx:A.b : A→B. →E: from Γ⊢f:A→B and Γ⊢a:A infer Γ⊢f a:B. Each variable occurs at most once in a context; two types are equal exactly when they are syntactically identical. - G3 — Target proposition S=P∧Q→Q∧P; the term to be read t=λh:P∧Q. ⟨snd h, fst h⟩; the comparison term t′=λh:P∧Q. ⟨fst h, snd h⟩. - G4 — Lean was not run for this guide (MKO assumption a2): there is no kernel verdict, no saved term and no receipt. - \Gamma_0,\ \Gamma_1 — the empty context; Γ0 extended by the hypothesis h:P∧Q - \Gamma\vdash u:A — judgment: in context Γ the term u has type A - \langle a,b\rangle — pair constructor (∧-introduction) - \mathrm{fst}\,p,\ \mathrm{snd}\,p — first and second projection (∧-elimination) - \lambda h{:}A.\,b — function abstraction over a hypothesis h:A (→-introduction) - S — the target proposition P∧Q→Q∧P - T(u) — the type derived for the term u in the given context ## Rules and sources - def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - imp_intro · prerequisite — →-introduction (discharging a hypothesis): if Q is derived inside a scope that temporarily assumes P, then P⇒Q follows, and P may no longer be used as known. - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable. - eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w. - modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q. - eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true. - case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility. - mko_proof_term · cited — Fix a Lean version, imports, environment E and local context Γ. If core term t has propositional type P and the kernel accepts Γ⊢t:P, then t is a proof term for P. A tactic log is a construction trace, not a saved, replayable proof-term receipt. · mko-lean-proof-term - mko_receipt · cited — A successful tactic run with no goals usually yields a candidate proof term; only saving that term and checking it with the specified kernel and environment forms a receipt. Kernel acceptance proves only the formal judgment; whether the statement is faithful and whether the imports contain improper axioms are separate obligations. · mko-lean-proof-term - st_var · prerequisite — Var rule of ST: if x:A is listed in Γ then Γ⊢x:A. - st_and_intro · prerequisite — ∧I rule of ST: from Γ⊢a:A and Γ⊢b:B infer Γ⊢⟨a,b⟩:A∧B; the type of the first component becomes the left conjunct. - st_and_elim · prerequisite — ∧E1 and ∧E2 rules of ST: from Γ⊢p:A∧B infer Γ⊢fst p:A and Γ⊢snd p:B. - st_imp_intro · prerequisite — →I rule of ST: from Γ,x:A⊢b:B infer Γ⊢λx:A.b : A→B; x no longer appears in the conclusion's context (the hypothesis is discharged). - st_type_eq · prerequisite — Type equality in ST is syntactic identity: A∧B≡C∧D ⇔ A≡C and B≡D; A→B≡C→D ⇔ A≡C and B≡D; distinct atoms are not equal. - L_inversion · lemma — Inversion for ST: each outer term form is the subject of the conclusion of exactly one rule. So if Γ⊢u:A is derivable, the last rule of the derivation is the rule for u's outer form, its premises are derivable, and A has the shape that rule prescribes. - L_tprime_untyped · lemma — In ST the judgment Γ0⊢t′:P∧Q→Q∧P is not derivable, where t′=λh:P∧Q. ⟨fst h, snd h⟩. ## Main derivation S01 · definitionBefore \text{proof term: fixed version, imports, environment }E,\ \Gamma,\ \text{kernel} After \text{ST: atoms }P\neq Q,\ \Gamma_0=\varnothing,\ S=P\land Q\to Q\land P,\ \text{six rules} Conditions: none Rule: mko_proof_term · Uses: G1, G2, G3, G4 Leaf basis: mko_proof_term + def_intro The MKO says that 'proof term' is meaningful only after the version, imports, environment and local context are fixed. This guide fixes a teaching counterpart: the environment E_ST contains only the atoms P and Q, the starting context Γ0 is empty, the target proposition is S=P∧Q→Q∧P, and the role of the checker is played by the six rules of G2: a judgment holds only if it can be derived rule by rule from them. Every typing conclusion below is a conclusion in ST; statements about Lean are handled separately in S10. S02 · definitionBefore t After t=\lambda h{:}P\land Q.\,\langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle Conditions: none Rule: def_intro · Uses: S01, G3 Leaf basis: def_intro + def_unfold Name the term and preview what each part is meant to establish: λh:P∧Q introduces a hypothesis named h of type P∧Q, read as 'assume a proof h of P∧Q'; fst h and snd h extract proofs of P and of Q from h; ⟨·,·⟩ packs two proofs into a proof of a conjunction, and the order of the components fixes the order of the conjuncts. Under propositions-as-types, a proof of an implication is a function that turns proofs of the premise into proofs of the conclusion. The Lean 4 surface counterpart is `fun h : P ∧ Q => And.intro h.right h.left` (or `fun h => ⟨h.2, h.1⟩`), given here only as a reading aid. S03 · impliesBefore \Gamma_1=\Gamma_0,\ h{:}P\land Q After \Gamma_1\vdash h:P\land Q Conditions: h{:}P\land Q\in\Gamma_1 Rule: st_var · Uses: S02, G2 Leaf basis: st_var The λ-binder says in which context the body is checked: Γ1 is Γ0 extended by h:P∧Q. By the Var rule, h:P∧Q is listed in Γ1, so Γ1⊢h:P∧Q. What this part establishes: inside the body, h may be used as a proof of P∧Q. S04 · impliesBefore \Gamma_1\vdash h:P\land Q After \Gamma_1\vdash \mathrm{snd}\,h:Q Conditions: A=P,\ B=Q Rule: st_and_elim · Uses: S03, G2 Leaf basis: st_and_elim Apply ∧E2 to S03 with A=P and B=Q: snd h extracts the second component and has type Q. This part establishes 'a proof of Q obtained from the hypothesis'. The type of snd h is read off from the type of h; it is not chosen freely. S05 · impliesBefore \Gamma_1\vdash h:P\land Q After \Gamma_1\vdash \mathrm{fst}\,h:P Conditions: A=P,\ B=Q Rule: st_and_elim · Uses: S03, G2 Leaf basis: st_and_elim Apply ∧E1 to S03: fst h extracts the first component and has type P. Now Γ1 has both a proof of P and a proof of Q, and both depend only on the hypothesis h. S06 · impliesBefore \Gamma_1\vdash \mathrm{snd}\,h:Q,\ \ \Gamma_1\vdash \mathrm{fst}\,h:P After \Gamma_1\vdash \langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:Q\land P Conditions: a=\mathrm{snd}\,h,\ A=Q,\ b=\mathrm{fst}\,h,\ B=P Rule: st_and_intro · Uses: S04, S05 Leaf basis: st_and_intro Apply ∧I with first component a=snd h (type A=Q) and second component b=fst h (type B=P), giving A∧B=Q∧P. The order of the conjuncts is fixed by the order of the components: the type of the first component becomes the left conjunct. This part establishes 'a proof of Q∧P from the hypothesis P∧Q'. S07 · impliesBefore \Gamma_0,\ h{:}P\land Q\vdash \langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:Q\land P After \Gamma_0\vdash \lambda h{:}P\land Q.\,\langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:P\land Q\to Q\land P Conditions: x=h,\ A=P\land Q,\ B=Q\land P Rule: st_imp_intro · Uses: S06, S03 Leaf basis: st_imp_intro + imp_intro Apply →I with x=h, A=P∧Q and B=Q∧P: the hypothesis h is discharged and the conclusion lives in Γ0, where h no longer appears. The binder's annotation P∧Q becomes the antecedent of the implication and the body's type Q∧P becomes its consequent. This is →-introduction (imp_intro) read through propositions-as-types: obtaining Q∧P inside the scope of the assumption P∧Q gives P∧Q→Q∧P. S08 · impliesBefore T(t)=P\land Q\to Q\land P,\ \ S=P\land Q\to Q\land P After T(t)\equiv S Conditions: none Rule: st_type_eq · Uses: S07, G3 Leaf basis: st_type_eq + eq_refl_symm_trans The MKO formula T(t)=P asks that the derived type be the proposition itself (here the proposition is called S to avoid a clash with the atom P). Compare symbol by symbol: antecedent P∧Q against P∧Q, consequent Q∧P against Q∧P; they are identical, so T(t)≡S in ST. Lean compares types up to definitional equality, a wider relation; ST uses syntactic identity only, so no conversion is used here. S09 · impliesBefore \Gamma_0\vdash t:T(t),\ \ T(t)\equiv S After t\ \text{is a proof term for }S\ \text{in ST} Conditions: none Rule: mko_proof_term · Uses: S07, S08, mko_proof_term Leaf basis: mko_proof_term + modus_ponens + eq_replace The MKO definition asks for two things: the term's type is the proposition, and the checker of the fixed environment accepts the judgment. In ST the checker is the rule table: each of S03 to S07 is one rule of G2, forming a complete derivation of Γ0⊢t:T(t), and S08 identifies T(t) with S, so Γ0⊢t:S is derivable, the ST counterpart of 'the kernel accepts Γ⊢t:P'. Hence t is a proof term for S in ST; that is all this step claims. S10 · impliesBefore t\ \text{proof term in ST};\ \text{Lean not run} After \text{Lean counterpart: candidate term, no kernel verdict, no receipt} Conditions: none Rule: mko_receipt · Uses: S09, G4, mko_receipt Leaf basis: mko_receipt + modus_ponens By the MKO, only a saved term checked by the specified kernel in the specified environment forms a receipt. G4 records that Lean was not run, and no term was saved or checked. So the Lean 4 counterpart `fun h : P ∧ Q => And.intro h.right h.left` has the status of a candidate proof term only: no kernel acceptance is claimed and there is no receipt. The ST derivation cannot replace a kernel verdict, because the two are different systems (Lean also has universes, definitional equality and an elaborator). Even if a kernel later accepted it, that would prove only the formal judgment; whether the proposition faithfully expresses the intended claim and whether the imports contain improper axioms still need separate review. S11 · impliesBefore \text{rule table of ST} After \text{each outer term form is concluded by exactly one rule} Conditions: none Rule: case_analysis · Uses: G2 Leaf basis: case_analysis + def_unfold Go through the six rules and record the outer form of the subject in each conclusion: Var, a variable; ∧I, a pair ⟨a,b⟩; ∧E1, fst p; ∧E2, snd p; →I, λx:A.b; →E, an application f a. Six rules, six pairwise distinct forms, and every term has exactly one outer form. A derivation of Γ⊢u:A ends with a rule whose conclusion is Γ⊢u:A, so its last rule is the unique rule for u's outer form, that rule's premises must have been derived above it, and A must have the shape the rule prescribes. This proves Lemma L_inversion. S12 · impliesBefore t'=\lambda h{:}P\land Q.\,\langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle After \Gamma_0\nvdash t':P\land Q\to Q\land P Conditions: none Rule: L_tprime_untyped · Uses: G3, L_tprime_untyped Leaf basis: L_inversion + st_type_eq + contradiction By Lemma L_tprime_untyped (proved in S12.1 to S12.4), t′ cannot have type S in ST. So t′ is not a proof term for S, even though it uses the same hypothesis and the same two projections. S13 · impliesBefore \Gamma_1\vdash \mathrm{fst}\,h:P,\ \ \Gamma_1\vdash \mathrm{snd}\,h:Q After \Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:P\land Q Conditions: a=\mathrm{fst}\,h,\ A=P,\ b=\mathrm{snd}\,h,\ B=Q Rule: st_and_intro · Uses: S04, S05 Leaf basis: st_and_intro See what t′ actually proves: with the components in the order fst h, snd h, ∧I gives P∧Q, not Q∧P. The only difference is the order of the components, and it changes the type. S14 · impliesBefore \Gamma_0,\ h{:}P\land Q\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:P\land Q After \Gamma_0\vdash t':P\land Q\to P\land Q Conditions: x=h,\ A=P\land Q,\ B=P\land Q Rule: st_imp_intro · Uses: S13 Leaf basis: st_imp_intro + imp_intro Apply →I to S13 and discharge h: t′ is a proof term for P∧Q→P∧Q, a different proposition. So whether a term proves S depends on its exact type, not on which hypotheses or projections it uses. S15 · impliesBefore \Gamma_0\vdash t:S,\ \Gamma_0\nvdash t':S,\ \text{Lean not run} After t\ \text{proves }S\ \text{in ST};\ t'\ \text{does not};\ \text{no Lean receipt} Conditions: none Rule: and_intro_elim · Uses: S09, S10, S12, S14 Leaf basis: and_intro_elim Combine the three conclusions: t is a proof term for S in ST (S09); t′ is not (S12), and proves P∧Q→P∧Q instead (S14); on the Lean side there is only a candidate term, with no kernel verdict and no receipt (S10). ## Substeps and lemmas S12.1 · impliesBefore \Gamma_0\vdash t':P\land Q\to Q\land P\ \ (\text{assumed}) After \Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:Q\land P Conditions: none Rule: L_inversion · Uses: G3, L_inversion Leaf basis: L_inversion + st_type_eq For contradiction, assume Γ0⊢t′:S has a derivation. The outer form of t′ is λ, so by L_inversion the last rule is →I; in its conclusion type A→B, A is the binder annotation P∧Q, and A→B≡P∧Q→Q∧P gives B≡Q∧P. So the premise Γ0,h:P∧Q⊢⟨fst h, snd h⟩:Q∧P is derivable, that is, Γ1⊢⟨fst h, snd h⟩:Q∧P. S12.2 · impliesBefore \Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:Q\land P After \Gamma_1\vdash \mathrm{fst}\,h:Q Conditions: none Rule: L_inversion · Uses: S12.1, L_inversion Leaf basis: L_inversion + st_type_eq A pair is concluded only by ∧I, whose conclusion type A∧B has A equal to the type of the first component. A∧B≡Q∧P gives A≡Q, so the premise Γ1⊢fst h:Q must be derivable. S12.3 · impliesBefore \Gamma_1\vdash \mathrm{fst}\,h:Q After \Gamma_1\vdash h:Q\land B\ \text{for some type }B Conditions: none Rule: L_inversion · Uses: S12.2, L_inversion Leaf basis: L_inversion The form fst is concluded only by ∧E1, whose premise is Γ1⊢h:A∧B with conclusion type A. Here A≡Q, so for some type B the judgment Γ1⊢h:Q∧B is derivable. S12.4 · impliesBefore \Gamma_1\vdash h:Q\land B After Q\land B\equiv P\land Q\Rightarrow Q\equiv P\ \ (\text{contradiction}) Conditions: P\not\equiv Q Rule: contradiction · Uses: S12.3, G1, G2, L_inversion Leaf basis: st_var + st_type_eq + contradiction A variable is concluded only by Var, so h:Q∧B must be exactly the entry for h in Γ1; Γ1 lists h once, with type P∧Q, so Q∧B≡P∧Q. Componentwise comparison by st_type_eq gives Q≡P, contradicting that P and Q are distinct atoms (G1). So the assumption of S12.1 fails and Γ0⊢t′:S is not derivable. S12.1 to S12.4 together prove Lemma L_tprime_untyped. ## Reverse audits - S15 · sufficient_goal_reduction · S09, S10, S12, S14, and_intro_elim — Goal G: the three determinations stated in the goal. Sufficient condition H: the three proved conclusions S09, S12 and S10 (H⇒G by conjunction introduction). H is derived forwards from the givens; G is never used as a premise. - S14 · premise_audit · S13, st_imp_intro — The same use of →I as in S07; together with S12, the type of t′ is P∧Q→P∧Q and cannot be S. - S13 · premise_audit · S04, S05, st_and_intro — It reuses the two judgments of S04 and S05, paired in the other order. - S12.4 · premise_audit · S12.3, G1, st_var, st_type_eq, contradiction — The contradiction needs two things: each variable occurs once in a context (G2), and P and Q are distinct (G1). If P and Q were the same atom, t′ would have type S, so this premise cannot be dropped. - S12.3 · premise_audit · S12.2, L_inversion — B is whatever type occurs in the premise of ∧E1; we need not know it. Still under the assumption made for contradiction. - S12.2 · premise_audit · S12.1, L_inversion, st_type_eq — It uses only inversion and componentwise comparison of conjunction types; it is still under the assumption made for contradiction. - S12.1 · premise_audit · L_inversion, st_type_eq — It uses that a λ-term is concluded only by →I and that A→B≡P∧Q→Q∧P forces B≡Q∧P. This is a temporary assumption of the proof by contradiction, discharged in S12.4. - S12 · premise_audit · L_tprime_untyped — It depends on the lemma, whose proof uses only inversion and the distinctness of P and Q. - S11 · premise_audit · G2, case_analysis — The case analysis is complete because G2 lists all rules of ST (exactly six). If the system had a conversion rule or a second rule for pairs, inversion would need more cases; that is one reason this argument cannot be moved to Lean unchanged. - S10 · premise_audit · G4, S09, mko_receipt — It needs only the fact that no kernel check took place. The direction is 'not checked ⇒ no receipt'; the step does not claim that Lean would reject the term either: it makes no claim at all about Lean's verdict. - S09 · premise_audit · S07, S08, mko_proof_term — It needs a complete derivation (one rule per step) and the type match. The conclusion belongs to ST only and is not transferred to Lean (see S10). - S08 · premise_audit · S07, G3, st_type_eq — It needs the type derived in S07 and the proposition from G3; what is compared is types, not truth values. Q∧P and P∧Q are logically equivalent but are not the same type (see the error controls). - S07 · premise_audit · S06, st_imp_intro, imp_intro — →I needs the body's judgment in the context Γ0 extended by exactly h:P∧Q, and S06 supplies precisely Γ1. After discharge, h may no longer be used as known. - S06 · premise_audit · S04, S05, st_and_intro — ∧I needs both premises in the same context, and S04 and S05 are both in Γ1. The type Q∧P is forced by the order of the components; swapping them gives P∧Q (see S13). - S05 · premise_audit · S03, st_and_elim — As in S04, only the conjunction type of h is needed; the result lies in the same context Γ1 as S04, which S06 requires. - S04 · premise_audit · S03, st_and_elim — ∧E2 needs h to have a conjunction type, and S03 supplies P∧Q. No converse is claimed: a proof of Q does not give a proof of P∧Q. - S03 · premise_audit · G2, st_var — Var needs only that h:P∧Q is listed in Γ1. No converse is claimed: h is not declared in Γ0, so Γ0⊢h:P∧Q fails, which is why the body must be checked in Γ1. - S02 · premise_audit · G3, def_intro — This step only names the term; the reading of its parts is a plan that S03 to S07 must justify rule by rule. No type of t is claimed yet. - S01 · premise_audit · G1, G2, G4, mko_proof_term — This step only fixes the setting and derives no new fact. Letting the ST rule table stand in for a kernel is a teaching choice stated in G2 and G4, not evidence about Lean. ## Error controls and negative controls Tactic logs, zero goals and self-reports are not receiptsA tactic script such as `intro h; exact ⟨h.2, h.1⟩` showing no remaining goals only says that the construction appears to be complete. By the MKO, a receipt needs the saved term and the result of a kernel check under the specified toolchain, imports and environment. A message reporting successful compilation, or a model's self-report, likewise cannot replace a saved, replayable kernel verdict. That is why S10 assigns only the candidate status. The type must match exactly, not merely mention P and Qt′ uses the same hypothesis and both projections, yet its type is P∧Q→P∧Q; S12 proves by inversion that it cannot have type S. Moreover Q∧P and P∧Q have the same truth value under every valuation (N2), but they are not the same type; their logical equivalence requires proofs in both directions. The term t establishes only P∧Q→Q∧P; a corresponding swap term is needed in the reverse direction. Even an established equivalence does not replace type comparison in this syntactic system. An ST derivation is not a Lean kernel checkST has six rules and syntactic equality only; Lean also has universes, definitional equality, elaboration and implicit arguments. The derivation here explains the structure of a proof term; it does not prove that any Lean file compiles. Even kernel acceptance proves only the formal judgment; whether the proposition is faithful and whether the imports contain improper axioms still need separate review (third paragraph of the MKO). - The tactic script `intro h; exact ⟨h.2, h.1⟩` shows no goals, so a kernel-accepted proof-term receipt exists → reject — Zero goals is a state of the construction; a receipt needs a saved term checked by the kernel in a specified environment, and neither exists here (G4, S10). - t′=λh:P∧Q. ⟨fst h, snd h⟩ is also a proof term for P∧Q→Q∧P, since it uses the same hypothesis and both projections → reject — By inversion this would require Q≡P, contradicting that P and Q are distinct (S12.4); the type of t′ is P∧Q→P∧Q (S14). - Since ⊢t:S is derivable in ST, Lean's kernel has accepted `fun h : P ∧ Q => And.intro h.right h.left` → reject — ST is a synthetic teaching system and Lean was not run; a derivation in one system is not the verdict of a different checker. - If the kernel accepts Γ⊢t:S, then S faithfully expresses the original Chinese statement and the imports contain no improper axioms → reject — The MKO says kernel acceptance proves only the formal judgment; faithfulness and the axiom inventory are separate semantic and trust obligations. ## Result and limitations In the synthetic system ST, the parts of t=λh:P∧Q. ⟨snd h, fst h⟩ establish in turn: h is a hypothesis of P∧Q, snd h and fst h are proofs of Q and P, the pair gives Q∧P, and discharging h gives P∧Q→Q∧P; this type is symbol for symbol the same as S, so t is a proof term for S in ST. The term t′=λh:P∧Q. ⟨fst h, snd h⟩ has type P∧Q→P∧Q and, by inversion, cannot have type S. Lean was not run: the Lean 4 counterpart is only a candidate, with no kernel verdict and no receipt. - N1 to N3 are truth-table checks over the four Boolean valuations, which are all the valuations; they concern classical truth values only, not typing, and the typing argument does not depend on them. - The →E rule is not used in the derivations here; it is listed so that the case analysis for inversion in S11 is complete. - A Lean receipt (fixed toolchain, imports, axiom inventory and saved term) is left until the OCME owner resumes Lean work. ## Verification and source binding 3 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: e911f6af08dca1ddcd82398376624ff01b2bc98988791c2202ae47e5512c751c - original source SHA-256: a17503af594b30f3d269250d35760be89786b5b022f96578e7977e5d3be7c2da - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-lean-proof-term-01.json)