induction_pr with arguments
Make a version of induction_pr with arguments.
"induction_pr H"
Same for "induction_ty_lex".
Edited by DAILLER Sylvain
Exceptional GitLab maintenance is scheduled for September 18, 2025. The service will be unavailable between 5:00 and 7:00 pm. Please do not work on the platform until an announcement indicates that maintenance is complete.
Make a version of induction_pr with arguments.
"induction_pr H"
Same for "induction_ty_lex".