Am I dreaming or Equations is renaming my hypothesis H ???
From Equations Require Import Equations.
Inductive vec A : nat -> Type :=
| vnil : vec A 0
| vcons : A -> forall (n : nat), vec A n -> vec A (S n).
Arguments vnil {_}.
Arguments vcons {_} _ _ _.
Equations vmap {A B} (f : A -> B) (n : nat) (v : vec A n) : vec B n :=
vmap f 0 vnil := vnil ;
vmap f (S n) (vcons a n v) := vcons (f a) n (vmap f n v).
Arguments vmap {_ _} _ {_} _.
Definition vmap_cong {A B n} (f f' : A -> B) (v : vec A n) :
(forall a, f a = f' a) -> vmap f v = vmap f' v.
Proof.
intros H. funelim (vmap f v); simp vmap.
- reflexivity.
- f_equal. easy. apply H.
Probably because it generalizes it first and forgets that it should not use "H" to introduce the induction hypothesis because a later hypothesis to be introduced uses it
Last updated: Oct 13 2024 at 01:02 UTC