 Logical disjunction

The disjunction $A\vee B$ holds when at least one of $A$ and $B$ holds. Constructively, a proof records which disjunct holds and provides its proof.