Goalforall b : bool, match b as b' returnif b' then True else True with true => I | false => I end = matchb as b' returnif b' then True else True with true => I | false => I end. intro.
lazymatch goalwith
| [ |- context[match ?b as b' in bool return @?P b' with true => ?t | false => ?f end] ]
=> change (match b as b' in bool return P b' with true => t | false => f end) with (@bool_rect P t f b) end. Abort.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
