proposition: Fact In_In_t x l (P : Prop) : (In_t x l -> P) -> In x l -> P.
proof: Proof. induction l as [ | y l IHl ]. + intros _ []. + intros H1 [ -> | H2 ]. * apply H1; simpl; auto. * apply IHl; auto. intros; apply H1; simpl; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)