IDENTITY

The identity predicate expresses numerical identity.

Systems

LRC_F

Typed Forward Strict

=E: Identity Elimination=I: Identity Introduction

Point And Click

=E: Identity Elimination=I: Identity Introduction

OLI

Point And Click

=I: Identity Introduction=E: Identity Elimination

The Logic Book

Point And Click

=E: Identity Elimination=I: Identity Introduction

LRC

Typed Forward Strict

=E: Identity Elimination=I: Identity Introduction

Point And Click

=E: Identity Elimination=I: Identity Introduction

LRC_P

Typed Forward Strict

=E: Identity Elimination=I: Identity Introduction

Point And Click

=E: Identity Elimination=I: Identity Introduction

LRC_O

Typed Forward Strict

=E: Identity Elimination=I: Identity Introduction

Point And Click

=E: Identity Elimination=I: Identity Introduction