theory Question
imports Main
begin

    datatype (discs_sels) 'a "term" =
      V 'a
    | U
    | T "'a term * 'a term"
    | C "'a term * 'a term"
    | L "'a term"
    | L' "'a term"
    | R "'a term"
    | R' "'a term"
    | A "'a term * 'a term * 'a term"
    | A' "'a term * 'a term * 'a term"

    primrec I :: "'a term \<Rightarrow> bool"
    where "I (V x) = True"
        | "I U = True"
        | "I (T tu) = (\<lambda>tu. fst tu \<and> snd tu) (map_prod I I tu)"
        | "I (C tu) = False"
        | "I (L t) = False"
        | "I (L' t) = False"
        | "I (R t) = False"
        | "I (R' t) = False"
        | "I (A tuv) = False"
        | "I (A' tuv) = False"

    fun F :: "'a term \<Rightarrow> 'a term"
    where "F (T (T (a, b), c)) = A (a, b, c)"
        | "F (T (U, b)) = L b"
        | "F (T (a, U)) = R a"
        | "F (T (a, b)) = (if I (F a) then T (a, F b) else T (F a, b))"
        | "F a = a"

    lemma
    assumes "\<not>is_T a" and "a \<noteq> U" and "b \<noteq> U"
    shows "F (T (a, b)) = (if I (F a) then T (a, F b) else T (F a, b))"
      sorry

end