To prove some lemma, I use the induct tactic. The base is accepts (multi A m vs) w ⟹ ∃us. Ball (set us) (accepts A) ∧ w = concat us ∧ length us = m
, and now I have accepts (multi A m vs) v
. Could I get the conclusion of ∃us. Ball (set us) (accepts A) ∧ v = concat us ∧ length us = m
proof (prove)
using this:
accepts (multi A m vs) v
accepts (multi A m vs) w ⟹ ∃us. Ball (set us) (accepts A) ∧ w = concat us ∧ length us = m
goal (1 subgoal):
A minimal working example perhaps?
Last updated: Dec 07 2024 at 16:22 UTC