Coqを使っていたら、coqcを落すコードに出会ってしまいました。 コード Require Import Sets.Ensembles. Variable (P: Prop). Variable (A: Type). Hypothesis the_hypo : forall x, exists xs, In A xs x -> P. Theorem some_theorem : P -> P. Proof. intr…