- support for atomic arities and candidates of reducibility started

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / term.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
index 376061b70bb52cef59e3b11c08cb920ab6ba42ff..42e7b8633a851ecc8e3bf93717455b62b5b3692a 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
@@ -42,9 +42,8 @@ lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False.
 #I #T #V elim V -V
 [ #J #H destruct
 | #J #W #U #IHW #_ #H destruct
-(*
- (generalize in match e1) -e1 >e0 normalize
-*) -I /2/ (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
+  -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
+  /2 width=1/
 ]
 qed-.
 
@@ -52,7 +51,9 @@ qed-.
 lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False.
 #I #V #T elim T -T
 [ #J #H destruct
-| #J #W #U #_ #IHU #H destruct -I V /2/ (**) (* destruct: the destucted equality is not erased *)
+| #J #W #U #_ #IHU #H destruct
+  -H (**) (* destruct: the destucted equality is not erased *)
+  /2 width=1/
 ]
 qed-.