Check for a type-confusion issue in IndDef

[talsewell]

Add an additional user-input check to InductiveRelation.check_clause to catch a case where different clauses of an inductive relation would give it different types. This would lead to low-level matching errors later in the process.

[talsewell]

I'm going to pull this PR, the proposal addresses an issue that I'd misunderstood.

The type inconsistency would already not be permitted if the user had typed it directly. It appears (deep in the code) because the inner machinery has inconsistently made adjustments for "schematic" variables in the relation.