def memn_append_l.go

minebender-game@1.0.0.0 · proof_cells.bend:114

import Base

114def memn_append_l.go(+x: Nat, +t: List<&2, Nat>, +ys: List<&2, Nat>, +i: Nat, +b: Bool,
115  e: {Bool.or(b, memn(t, i)) == True{} : Bool},
116  ih: {memn(t, i) == True{} : Bool} -> {memn(List.append(&2, Nat, t, ys), i) == True{} : Bool}) ->
117  {Bool.or(b, memn(List.append(&2, Nat, t, ys), i)) == True{} : Bool}:
118  match b:
119    case True{}:
120      {==}
121    case False{}:
122      ih(e)