proposition: Lemma cast_fun P Q (f : forall n, P n -> Q n) n k (v : P n) (H : n = k) : f _ (cast v H) = cast (f _ v) H.
proof: Proof. subst; auto. Qed.
imports: List Arith Lia Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_list finite)