@@ -1,8 +1,5 @@
11module prelude.list
22
3−import prelude.maybe
4−import builtins
5−
63%access public
74
85import builtins
@@ -467,59 +464,59 @@ hasAnyNilFalse l = ?hasAnyNilFalseBody
467464-- Proofs
468465--------------------------------------------------------------------------------
469466
470−MoreList.lengthAppendStepCase = proof {
467+lengthAppendStepCase = proof {
471468 intros;
472469 rewrite inductiveHypothesis;
473470 trivial;
474471}
475472
476−MoreList.hasAnyNilFalseBody = proof {
473+hasAnyNilFalseBody = proof {
477474 intros;
478475 rewrite (hasAnyByNilFalse (==) l);
479476 trivial;
480477}
481478
482−MoreList.hasAnyByNilFalseStepCase = proof {
479+hasAnyByNilFalseStepCase = proof {
483480 intros;
484481 rewrite inductiveHypothesis;
485482 trivial;
486483}
487484
488−MoreList.initProof = proof {
485+initProof = proof {
489486 intros;
490487 trivial;
491488}
492489
493−MoreList.lastProof = proof {
490+lastProof = proof {
494491 intros;
495492 trivial;
496493}
497494
498−MoreList.appendNilRightNeutralStepCase = proof {
495+appendNilRightNeutralStepCase = proof {
499496 intros;
500497 rewrite inductiveHypothesis;
501498 trivial;
502499}
503500
504−MoreList.appendAssociativeStepCase = proof {
501+appendAssociativeStepCase = proof {
505502 intros;
506503 rewrite inductiveHypothesis;
507504 trivial;
508505}
509506
510−MoreList.mapFusionStepCase = proof {
507+mapFusionStepCase = proof {
511508 intros;
512509 rewrite inductiveHypothesis;
513510 trivial;
514511}
515512
516−MoreList.mapDistributesOverAppendStepCase = proof {
513+mapDistributesOverAppendStepCase = proof {
517514 intros;
518515 rewrite inductiveHypothesis;
519516 trivial;
520517}
521518
522−MoreList.mapPreservesLengthStepCase = proof {
519+mapPreservesLengthStepCase = proof {
523520 intros;
524521 rewrite inductiveHypothesis;
525522 trivial;