added discriminate to the boolean_eq tactic in Common.v
unrolled tac tactic in circuit proofs and trying to research the cause of the need for discriminate etc