version of the tac tactic for proving circuits in Examples/Doors incorporating simpl
fixing applications of inl in Examples/Doors.v
fixing applications of inl in Examples/MoreDoors.v
needed to use simpl before intros_all again in Examples/Muxer.v
applying semantics of Mux before realising circuits