Follow-ups from the review of #22: a repeated proof block, and two meanings of replyLaw #31

Two points from the review of #22, left for later.

1. RandomSystem.ofProbAutomaton_eq_drawStep and PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton (Converter/ProbProgramAttachment.lean) repeat the same proof block: the invariant of the recording automaton, its preservation (hpres) and its initial case (hinit). These could be two lemmas used by both theorems.

2. ProbStep.replyLaw (the reply law of an automaton from a state law) and Program.replyLaw (the reply law of one program invocation against fresh samples) share a name. System/Memoryless.lean uses both. One should be renamed; candidate names to be proposed here first.