def AP.one_elem

bend-osdev-array@0.1.0.1 · PROOF.bend:1424

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1424def AP.one_elem(-T: Data, xs: List<&2, T>, -f: T, h: {List.length(&2, T, xs) == 1n : Nat}) -> {Con{A.Arrays.nth(T, xs, 0n, f), Nil{}} == xs : List<&2, T>}:
1425  match xs:
1426    case Nil{}:
1427      Empty.absurd({Con{A.Arrays.nth(T, Nil{}, 0n, f), Nil{}} == Nil{} : List<&2, T>}, AP.sz(0n, Equal.sym(Nat, 0n, 1n, h)))
1428    case Con{x, t}:
1429      match t:
1430        case Nil{}:
1431          {==}
1432        case Con{y, u}:
1433          Empty.absurd({Con{A.Arrays.nth(T, Con{x, Con{y, u}}, 0n, f), Nil{}} == Con{x, Con{y, u}} : List<&2, T>}, AP.sz(List.length(&2, T, u), AP.pred_cong(1n+List.length(&2, T, u), 0n, h)))