fact: Definition econs_ar ar p : Econs (p ar) (nat -> forall ar, p ar) := fun x env n => match n with | 0 => fun ar' => match Nat.eq_dec ar ar' with | left e => match e in _ = ar' return p ar' with eq_refl => x end | right _ => env n ar' end | S n => fun ar' => if Nat.eq_dec ar ar' then env n ar' else env (S n) ar' end.
imports: Vector Arith