proposition: Lemma beq_list_comm: forall bs1 bs2, RAWBITVECTOR_LIST.beq_list bs2 bs1 = RAWBITVECTOR_LIST.beq_list bs1 bs2.
proof: Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1]. - intros. case bs2. easy. intros. easy. - intros. case bs2. easy. intros. simpl. specialize (@IHbs1 l). rewrite IHbs1. case (RAWBITVECTOR_LIST.beq_list xsbs1 l). do 2 rewrite andb_true_r. unfold Bool.eqb. case b. easy. easy. now do 2 rewrite andb_false_r. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance