The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Definition fin limit := {n | n <= limit}.

Definition vect A limit := fin limit -> A.

Definition fin_zero limit: fin limit.

 exists O; induction limit; auto.

Defined.

Definition aux3 {n} (v1 v2: vect bool n):

  (forall i, projT1 i <= O -> v1 i = false \/ v2 i = false) -> andb (v1 (fin_zero n)) (v2 (fin_zero n)) = false.

 intros. destruct (H (fin_zero n) (le_n O)).

 rewrite H0.

(* Error: Found no subterm matching "v1 (fin_zero n)" in the current goal. *)

(* Goal: (v1 (fin_zero n) && v2 (fin_zero n))%bool = false *)