def ga_con

bendtorch@1.3.0.0 · PROOF.bend:331

import Base
import bendtorch@1.3.0.0/main.bend as T

331def ga_con(x: T.FS, -t: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>, r: GAR<t, x <> b, c>) -> GAR<x <> t, b, c>:
332  match r:
333    case GAR{ys, same, fact}:
334      GAR{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact}