Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022)