def off.lat_app_lt

bend-osdev-bytes@0.1.1.0 · PROOF.bend:996

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

996def off.lat_app_lt(+i: Nat, a: List<&2, U32>, +b: List<&2, U32>) -> {Nat.is_lt(i, B.len(a)) == True{} : Bool} -> {B.at(B.append(a, b), i) == B.at(a, i) : Maybe<&2, U32>}:
997  match i a:
998    case 0n Nil{}:
999      h => off.no({B.at(b, 0n) == None{} : Maybe<&2, U32>}, h)
1000    case 1n+p Nil{}:
1001      h => off.no({B.at(b, 1n+p) == B.at(Nil{}, 1n+p) : Maybe<&2, U32>}, h)
1002    case 0n Con{x, t}:
1003      h => {==}
1004    case 1n+p Con{x, t}:
1005      h => off.lat_app_lt(p, t, b, h)