justification we proved term ( id )

tmust have type Prop.

It derives t using the justification and labels the conclusion with id.

None.