definition hide ≝ λT:Type.λx:T.x.
notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
-interpretation "hide" 'hide =
- (cic:/matita/dama/property_sigma/hide.con _ _).
-interpretation "hide2" 'hide =
- (cic:/matita/dama/property_sigma/hide.con _ _ _).
+interpretation "hide" 'hide = (hide _ _).
+interpretation "hide2" 'hide = (hide _ _ _).
definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
coercion cic:/matita/dama/property_sigma/inject.con 0 1.
apply (trans_increasing ?? H4); intro; whd in H12;
apply (not_le_Sn_n i); apply (transitive_le ??? H12 H5)]
clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
-generalize in match (refl_eq nat (m q));
-generalize in match (m q) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H12:(? ? ? %); simplify in ⊢ (? ? (? ? ? % ?));
-generalize in match (refl_eq nat (m r));
-generalize in match (m r) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H14:(? ? ? %); simplify in ⊢ (? ? (? ? ? ? %));
generalize in match (refl_eq nat (m p));
-generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H16:(? ? ? %);
-apply H15; [3: apply le_n] destruct H16; destruct H14; destruct H12; clear H11 H13 H15;
+generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
+intros (H16); simplify in H16:(? ? ? %); destruct H16;
+apply H15; [3: apply le_n]
[1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
apply (le_to_not_lt p q H5);
|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
apply (le_to_not_lt p r H10);]
-qed.
\ No newline at end of file
+qed.