[STATEMENT]
lemma wf_indexlt_rel: "wf indexlt_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf indexlt_rel
[PROOF STEP]
using indexlt_rel_def pair_less_def
[PROOF STATE]
proof (prove)
using this:
indexlt_rel = less_than <*lex*> less_than
pair_less = less_than <*lex*> less_than

goal (1 subgoal):
 1. wf indexlt_rel
[PROOF STEP]
by auto