theorem lreceq3d (_G: wff) (z: nat) (S: set) (_n1 _n2: nat): $ _G -> _n1 = _n2 $ > $ _G -> lrec z S _n1 = lrec z S _n2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd | _G -> z = z |
|
2 | eqsidd | _G -> S == S |
|
3 | hyp _h | _G -> _n1 = _n2 |
|
4 | 1, 2, 3 | lreceqd | _G -> lrec z S _n1 = lrec z S _n2 |