I figure out that one can print them (the lambda terms) with `Show proof.`

in the middle of a proof (proof mode) and `Print lemma_name`

but I wasn’t able to actually give one. I won;t print all different attempts I did but here are a few of the identity function/P->P implication I did:

```
thm_identity' := fun (P : Type) (X : P) => X
: forall P : Type, P -> P.
Lemma thm_identity2 : forall (P:Type), P -> P :=
fun (P : Type) (X : P) => X.
Lemma thm_identity2 : forall (P:Type), P -> P :=
fun x => x.
```

but it won’t accept them even though I used the printed lambda term of my theorem…any help?

rest of my script:

```
Definition my_id1 {A:Type} (a:A) := a.
Compute my_id1 2.
Compute my_id1 3.
Print my_id1.
Definition my_id1' (A:Type) (a:A) := a.
Compute my_id1' nat 2.
Lemma thm_identity : forall (P:Type), P -> P.
Proof.
intros.
Show Proof.
assumption.
Show Proof.
Qed.
Print thm_identity.
thm_identity' := fun (P : Type) (X : P) => X
: forall P : Type, P -> P.
Lemma thm_identity2 : forall (P:Type), P -> P :=
fun (P : Type) (X : P) => X.
Lemma thm_identity2 : forall (P:Type), P -> P :=
fun x => x.
```