[STATEMENT]
lemma term_variants_pred_inv':
  assumes "term_variants_pred P (Fun f T) t"
  shows "is_Fun t"
    and "length T = length (args t)"
    and "\<And>i. i < length T \<Longrightarrow> term_variants_pred P (T ! i) (args t ! i)"
    and "f \<noteq> the_Fun t \<Longrightarrow> the_Fun t \<in> set (P f)"
    and "P \<equiv> (\<lambda>_. [])(g := [h]) \<Longrightarrow> f \<noteq> the_Fun t \<Longrightarrow> f = g \<and> the_Fun t = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_Fun t &&& length T = length (args t)) &&& (\<And>i. i < length T \<Longrightarrow> term_variants_pred P (T ! i) (args t ! i)) &&& (f \<noteq> the_Fun t \<Longrightarrow> the_Fun t \<in> set (P f)) &&& (\<lbrakk>P \<equiv> (\<lambda>_. [])(g := [h]); f \<noteq> the_Fun t\<rbrakk> \<Longrightarrow> f = g \<and> the_Fun t = h)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
term_variants_pred P (Fun f T) t

goal (1 subgoal):
 1. (is_Fun t &&& length T = length (args t)) &&& (\<And>i. i < length T \<Longrightarrow> term_variants_pred P (T ! i) (args t ! i)) &&& (f \<noteq> the_Fun t \<Longrightarrow> the_Fun t \<in> set (P f)) &&& (\<lbrakk>P \<equiv> (\<lambda>_. [])(g := [h]); f \<noteq> the_Fun t\<rbrakk> \<Longrightarrow> f = g \<and> the_Fun t = h)
[PROOF STEP]
by (auto elim: term_variants_pred.cases)