theorem sublistAteq3 (n L1 _L21 _L22: nat): $ _L21 = _L22 -> (sublistAt n L1 _L21 <-> sublistAt n L1 _L22) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _L21 = _L22 -> _L21 = _L22 |
|
2 | 1 | sublistAteq3d | _L21 = _L22 -> (sublistAt n L1 _L21 <-> sublistAt n L1 _L22) |