name specifications added for elim_intros, elim_intros_simpl and elim_type

[helm.git] / helm / matita / tests / fguidi.ma

diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index e42de00b50a9a530542696c461ae945caaa2459f..141e29776d009f8871290631e8c300ab01ddcad6 100644 (file)
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -94,5 +94,12 @@ qed.
 theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
 intros 1.
 elim x. auto.
-fwd H1 [].
+fwd H1 [H0]. 
+elim H0 names [pippo; pappo].
+
+decompose H0 
+
+
+elim H0. clear H0. elim H1. clear H1.
+
 *)