proposition: Lemma concat_nil: forall {A} (a: list A), a ++ [] = a.
proof: Proof. intros A a. case a; [ easy | intros; apply app_nil_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