proposition: Lemma afold_right_length_2 : forall A default OP t, (length t =? 2) = true -> afold_right A default OP t = OP (t.[0]) (t.[1]).
proof: Proof. intros A default OP t H; unfold afold_right; rewrite eqb_spec in H; rewrite H; change (2 =? 0) with false; reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz