proposition: Lemma well_founded_vector_direct_subterm' : forall A : Type, EqDec A -> WellFounded (t_subterm A).
proof: Proof. intros. apply Transitive_Closure.wf_clos_trans. intro. simp_sigmas. induction a0; constructor; intros; simp_sigmas. simpl in *. depelim H. depelim H. apply IHa0. Defined.
imports: Equations.Prop.Equations Bvector