include "basic_2/grammar/term_simple.ma".
(* SAME TOP TERM CONSTRUCTOR ************************************************)
include "basic_2/grammar/term_simple.ma".
(* SAME TOP TERM CONSTRUCTOR ************************************************)
lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2).
* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ]
lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2).
* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ]