proposition: Lemma t_ind : forall (P : forall n : nat, t n -> Prop), P 0 nil -> (forall (h : char) (n : nat) (v : t n), P n v -> P (S n) (cons h v)) -> forall (n : nat) (v : t n), P n v.
proof: Proof. intros. induction v; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Arith.Peano_dec Coq.Logic.Eqdep_dec Coq.ZArith.ZArith Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.BinLib.Core Bedrock.Word