Add begin-irrefl reasoning combinator
#1470
Merged
begin-irrefl reasoning combinator
#1470