proposition: Fact list_prod_spec X Y l m c : In c (@list_prod X Y l m) <-> In (fst c) l /\ In (snd c) m.
proof: Proof. revert c; induction l as [ | x l IHl ]; intros c; simpl; try tauto. rewrite in_app_iff, IHl, in_map_iff; simpl. split. + intros [ (y & <- & ?) | (? & ?) ]; simpl; auto. + intros ([ -> | ] & ? ); destruct c; simpl; firstorder. Qed.
imports: List Arith Lia Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec)