proposition: Lemma fast_length_length : forall {A} (l : list A), length l = fast_length l.
proof: Proof. apply (fast_length_elim (fun A l res => length l = res) (fun A l res l' lenl => res + length l' = lenl)); intros l H; simpl in *; intuition auto with arith; lia. Qed.