Rodin Handbook





 

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