4.4.3 What do the labels on the proof tree mean?

• ah means add hypothesis,

• eh means rewrite with equality from hypothesis from left to right,

• he means rewrite with equality from hypothesis from right to left,

• rv tells us that this goal has been manually reviewed (3.1.7.4),

• sl/ds means selection/deselection,

• PP means discharged by the predicate prover,

• ML means discharged by the mono lemma prover