proposition: Lemma to_list_two: forall {A:Type} (a: PArray.array A), PArray.length a = 2 -> (to_list a) = a .[0] :: a .[1] :: nil.
proof: Proof. intros A a H. unfold to_list. rewrite H. rewrite 2!foldi_lt_r by reflexivity. rewrite foldi_ge by reflexivity. reflexivity. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance