Inductive Simps.ProjectionRule

Modification history