feat(Circuit): sequential and parallel composition of circuits

[SamuelSchlesinger]

Program.append continues a program by a second one whose inputs are read from wires of the first. Feeding it the outputs gives Circuit.comp, feeding it the inputs gives Circuit.append on shared inputs. Both evaluate as expected and add gate counts.

Also adds Circuit.ComputesOn, computing a function on a support, as Set.EqOn, with composition and pairing lemmas for it and for Computes; Wire.castAdd for embedding wires into a continued program; and two Fin.append simp lemmas.

Based on #949.

[SamuelSchlesinger]

Reopened from an in-repo branch so it can be stacked on #949.