proposition: Fact fin_t_sum X Y (P Q : _ -> Prop) : @fin_t X P -> @fin_t Y Q -> fin_t (fun z : X + Y => match z with inl x => P x | inr y => Q y end).
proof: Proof. intros (l & Hl) (m & Hm). exists (map inl l ++ map inr m). intros z; rewrite in_app_iff, in_map_iff, in_map_iff. destruct z as [ x | y ]; [ rewrite Hl | rewrite Hm ]. + split. * left; exists x; auto. * intros [ (z & E & ?) | (z & C & _) ]; try discriminate; inversion E; subst; auto. + split. * right; exists y; auto. * intros [ (z & C & _) | (z & E & ?) ]; try discriminate; inversion E; subst; auto. 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)