theorem sublistAteq2 (n _L11 _L12 L2: nat): $ _L11 = _L12 -> (sublistAt n _L11 L2 <-> sublistAt n _L12 L2) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _L11 = _L12 -> _L11 = _L12 |
|
2 | 1 | sublistAteq2d | _L11 = _L12 -> (sublistAt n _L11 L2 <-> sublistAt n _L12 L2) |