theorem sublistAteq1 (_n1 _n2 L1 L2: nat): $ _n1 = _n2 -> (sublistAt _n1 L1 L2 <-> sublistAt _n2 L1 L2) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _n1 = _n2 -> _n1 = _n2 |
|
2 | 1 | sublistAteq1d | _n1 = _n2 -> (sublistAt _n1 L1 L2 <-> sublistAt _n2 L1 L2) |