lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
#T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ]
[1,4: @or_intror #H destruct
lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
#T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ]
[1,4: @or_intror #H destruct